Subject: Ssreflect Users Discussion List
List archive
- 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.