Skip to Content.
Sympa Menu

ssreflect - RE: Ltac + let:

Subject: Ssreflect Users Discussion List

List archive

RE: Ltac + let:


Chronological Thread 
  • From: Georges Gonthier <>
  • To: "" <>
  • Subject: RE: Ltac + let:
  • Date: Tue, 27 May 2008 19:12:21 +0100
  • Accept-language: en-US
  • Acceptlanguage: en-US


> I apologize for this too concise formulation: you are right that
> ssreflect in an extension of Coq, but the choices made on keywords, and
> more generally on syntax interact with the pre-existing, standard Coq
> tactic language Ltac.

Actually the Ltac and Gallina grammars are disjoint in Coq, and the ssreflect
let: extension only concerns the Gallina specification language.
As Assia indicated in her excellent answer, Ltac requires you to put a
constr: keyword to indicate that you want to parse a Gallina term rather than
an Ltac tactic expression.

At any rate, ssreflect only introduces the let: abbreviation for the Gallina
match. This is why your code raised a syntax error.

-- Georges



  • Ltac + let:, Assia Mahboubi, 05/26/2008
    • RE: Ltac + let:, Georges Gonthier, 05/27/2008

Archive powered by MHonArc 2.6.18.

Top of Page