aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/doc/changes.txt7
-rw-r--r--parsing/g_constr.ml4111
-rw-r--r--parsing/g_vernac.ml430
-rw-r--r--parsing/pcoq.ml47
-rw-r--r--parsing/pcoq.mli7
-rw-r--r--plugins/subtac/g_subtac.ml413
-rw-r--r--tactics/rewrite.ml430
7 files changed, 101 insertions, 104 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 1321b4978..4617f4dee 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -22,6 +22,13 @@ generally fewer than the defined ones.
whd_castappevar is now whd_head_evar
obsolete whd_ise disappears
+** Restructuration of the syntax of binders **
+
+binders_let -> binders
+binders_let_fixannot -> binders_fixannot
+binder_let -> closed_binder (and now covers only bracketed binders)
+binder was already obsolete and has been removed
+
** Semantical change of h_induction_destruct **
Warning, the order of the isrec and evar_flag was inconsistent and has
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index ef18ad4eb..087ae31ae 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -31,7 +31,7 @@ let mk_cast = function
(c,(_,None)) -> c
| (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty))
-let loc_of_binder_let = function
+let loc_of_binder = function
| LocalRawAssum ((loc,_)::_,_,_)::_ -> loc
| LocalRawDef ((loc,_),_)::_ -> loc
| _ -> dummy_loc
@@ -87,8 +87,8 @@ let lpar_id_coloneq =
| _ -> err ())
| _ -> err ())
-let impl_ident =
- Gram.Entry.of_parser "impl_ident"
+let impl_ident_head =
+ Gram.Entry.of_parser "impl_ident_head"
(fun strm ->
match get_tok (stream_nth 0 strm) with
| KEYWORD "{" ->
@@ -129,8 +129,8 @@ let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None
GEXTEND Gram
GLOBAL: binder_constr lconstr constr operconstr sort global
constr_pattern lconstr_pattern Constr.ident
- binder binder_let binders_let record_declaration
- binders_let_fixannot typeclass_constraint pattern appl_arg;
+ closed_binder binders binders_fixannot
+ record_declaration typeclass_constraint pattern appl_arg;
Constr.ident:
[ [ id = Prim.ident -> id
@@ -232,13 +232,13 @@ GEXTEND Gram
(id, Topconstr.abstract_constr_expr c (binders_of_lidents params)) ] ]
;
binder_constr:
- [ [ forall; bl = binder_list; ","; c = operconstr LEVEL "200" ->
+ [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" ->
mkCProdN loc bl c
- | lambda; bl = binder_list; [ "=>" | "," ]; c = operconstr LEVEL "200" ->
+ | lambda; bl = open_binders; [ "=>" | "," ]; c = operconstr LEVEL "200" ->
mkCLambdaN loc bl c
- | "let"; id=name; bl = binders_let; ty = type_cstr; ":=";
+ | "let"; id=name; bl = binders; ty = type_cstr; ":=";
c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
- let loc1 = loc_of_binder_let bl in
+ let loc1 = loc_of_binder bl in
CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
| "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
let fixp = mk_single_fix fx in
@@ -296,7 +296,7 @@ GEXTEND Gram
| "cofix" -> false ] ]
;
fix_decl:
- [ [ id=identref; bl=binders_let_fixannot; ty=type_cstr; ":=";
+ [ [ id=identref; bl=binders_fixannot; ty=type_cstr; ":=";
c=operconstr LEVEL "200" ->
(id,fst bl,snd bl,c,ty) ] ]
;
@@ -363,15 +363,7 @@ GEXTEND Gram
| n = INT -> CPatPrim (loc, Numeral (Bigint.of_string n))
| s = string -> CPatPrim (loc, String s) ] ]
;
- binder_list:
- [ [ idl=LIST1 name; bl=binders_let ->
- LocalRawAssum (idl,Default Explicit,CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))))::bl
- | idl=LIST1 name; ":"; c=lconstr ->
- [LocalRawAssum (idl,Default Explicit,c)]
- | cl = binders_let -> cl
- ] ]
- ;
- binder_assum:
+ impl_ident_tail:
[ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(loc, None))
| idl=LIST1 name; ":"; c=lconstr; "}" ->
(fun id -> LocalRawAssum (id::idl,Default Implicit,c))
@@ -388,47 +380,56 @@ GEXTEND Gram
rel=OPT constr; "}" -> (id, CMeasureRec (m,rel))
] ]
;
- binders_let_fixannot:
- [ [ id=impl_ident; assum=binder_assum; bl = binders_let_fixannot ->
- (assum (loc, Name id) :: fst bl), snd bl
- | f = fixannot -> [], f
- | b = binder_let; bl = binders_let_fixannot -> b @ fst bl, snd bl
- | -> [], (None, CStructRec)
+ binders_fixannot:
+ [ [ id = impl_ident_head; assum = impl_ident_tail; bl = binders_fixannot ->
+ (assum (loc, Name id) :: fst bl), snd bl
+ | f = fixannot -> [], f
+ | b = binder; bl = binders_fixannot -> b @ fst bl, snd bl
+ | -> [], (None, CStructRec)
] ]
;
- binders_let:
- [ [ b = binder_let; bl = binders_let -> b @ bl
- | -> [] ] ]
- ;
- binder_let:
- [ [ id=name ->
- [LocalRawAssum ([id],Default Explicit,CHole (loc, None))]
- | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
- [LocalRawAssum (id::idl,Default Explicit,c)]
- | "("; id=name; ":"; c=lconstr; ")" ->
- [LocalRawAssum ([id],Default Explicit,c)]
- | "("; id=name; ":="; c=lconstr; ")" ->
- [LocalRawDef (id,c)]
- | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
- [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))]
- | "{"; id=name; "}" ->
- [LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
- | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
- [LocalRawAssum (id::idl,Default Implicit,c)]
- | "{"; id=name; ":"; c=lconstr; "}" ->
- [LocalRawAssum ([id],Default Implicit,c)]
- | "{"; id=name; idl=LIST1 name; "}" ->
- List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
- | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
- List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
- | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
- List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
+ open_binders:
+ (* Same as binders but parentheses around a closed binder are optional if
+ the latter is unique *)
+ [ [ (* open binder *)
+ idl = LIST1 name; ":"; c = lconstr ->
+ [LocalRawAssum (idl,Default Explicit,c)]
+ (* binders factorized with open binder *)
+ | idl = LIST1 name; bl = binders ->
+ let t = CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))) in
+ LocalRawAssum (idl,Default Explicit,t)::bl
+ | bl = closed_binder; bl' = binders ->
+ bl@bl'
] ]
;
+ binders:
+ [ [ l = LIST0 binder -> List.flatten l ] ]
+ ;
binder:
- [ [ id=name -> ([id],Default Explicit,CHole (loc, None))
- | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c)
- | "{"; idl=LIST1 name; ":"; c=lconstr; "}" -> (idl,Default Implicit,c)
+ [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (loc, None))]
+ | bl = closed_binder -> bl ] ]
+ ;
+ closed_binder:
+ [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
+ [LocalRawAssum (id::idl,Default Explicit,c)]
+ | "("; id=name; ":"; c=lconstr; ")" ->
+ [LocalRawAssum ([id],Default Explicit,c)]
+ | "("; id=name; ":="; c=lconstr; ")" ->
+ [LocalRawDef (id,c)]
+ | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
+ [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))]
+ | "{"; id=name; "}" ->
+ [LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
+ | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
+ [LocalRawAssum (id::idl,Default Implicit,c)]
+ | "{"; id=name; ":"; c=lconstr; "}" ->
+ [LocalRawAssum ([id],Default Implicit,c)]
+ | "{"; id=name; idl=LIST1 name; "}" ->
+ List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
+ | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
+ List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
+ | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
+ List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
] ]
;
typeclass_constraint:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 359d2321d..3e5a52e46 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -141,9 +141,9 @@ GEXTEND Gram
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
- [ [ thm = thm_token; id = identref; bl = binders_let; ":"; c = lconstr;
+ [ [ thm = thm_token; id = identref; bl = binders; ":"; c = lconstr;
l = LIST0
- [ "with"; id = identref; bl = binders_let; ":"; c = lconstr ->
+ [ "with"; id = identref; bl = binders; ":"; c = lconstr ->
(Some id,(bl,c,None)) ] ->
VernacStartTheoremProof (thm,(Some id,(bl,c,None))::l, false, no_hook)
| stre = assumption_token; nl = inline; bl = assum_list ->
@@ -177,7 +177,7 @@ GEXTEND Gram
;
gallina_ext:
[ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref;
- ps = binders_let;
+ ps = binders;
s = OPT [ ":"; s = lconstr -> s ];
cfs = [ ":="; l = constructor_list_or_record_decl -> l
| -> RecordDecl (None, []) ] ->
@@ -238,13 +238,13 @@ GEXTEND Gram
;
(* Simple definitions *)
def_body:
- [ [ bl = binders_let; ":="; red = reduce; c = lconstr ->
+ [ [ bl = binders; ":="; red = reduce; c = lconstr ->
(match c with
CCast(_,c, Rawterm.CastConv (k,t)) -> DefineBody (bl, red, c, Some t)
| _ -> DefineBody (bl, red, c, None))
- | bl = binders_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
+ | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
DefineBody (bl, red, c, Some t)
- | bl = binders_let; ":"; t = lconstr ->
+ | bl = binders; ":"; t = lconstr ->
ProveBody (bl, t) ] ]
;
reduce:
@@ -261,7 +261,7 @@ GEXTEND Gram
;
(* Inductives and records *)
inductive_definition:
- [ [ id = identref; oc = opt_coercion; indpar = binders_let;
+ [ [ id = identref; oc = opt_coercion; indpar = binders;
c = OPT [ ":"; c = lconstr -> c ];
":="; lc = constructor_list_or_record_decl; ntn = decl_notation ->
(((oc,id),indpar,c,lc),ntn) ] ]
@@ -288,13 +288,13 @@ GEXTEND Gram
(* (co)-fixpoints *)
rec_definition:
[ [ id = identref;
- bl = binders_let_fixannot;
+ bl = binders_fixannot;
ty = type_cstr;
def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ]
;
corec_definition:
- [ [ id = identref; bl = binders_let; ty = type_cstr;
+ [ [ id = identref; bl = binders; ty = type_cstr;
def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
((id,bl,ty,def),ntn) ] ]
;
@@ -335,12 +335,12 @@ GEXTEND Gram
[ [ bd = record_binder; ntn = decl_notation -> bd,ntn ] ]
;
record_binder_body:
- [ [ l = binders_let; oc = of_type_with_opt_coercion;
+ [ [ l = binders; oc = of_type_with_opt_coercion;
t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN loc l t))
- | l = binders_let; oc = of_type_with_opt_coercion;
+ | l = binders; oc = of_type_with_opt_coercion;
t = lconstr; ":="; b = lconstr -> fun id ->
(oc,DefExpr (id,mkCLambdaN loc l b,Some (mkCProdN loc l t)))
- | l = binders_let; ":="; b = lconstr -> fun id ->
+ | l = binders; ":="; b = lconstr -> fun id ->
match b with
| CCast(_,b, Rawterm.CastConv (_, t)) ->
(false,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t)))
@@ -363,7 +363,7 @@ GEXTEND Gram
;
constructor_type:
- [[ l = binders_let;
+ [[ l = binders;
t= [ coe = of_type_with_opt_coercion; c = lconstr ->
fun l id -> (coe,(id,mkCProdN loc l c))
| ->
@@ -538,7 +538,7 @@ GEXTEND Gram
t = class_rawexpr ->
VernacCoercion (use_locality_exp (), ByNotation ntn, s, t)
- | IDENT "Context"; c = binders_let ->
+ | IDENT "Context"; c = binders ->
VernacContext c
| IDENT "Instance"; namesup = instance_name; ":";
@@ -588,7 +588,7 @@ GEXTEND Gram
| IDENT "transparent" -> Conv_oracle.transparent ] ]
;
instance_name:
- [ [ name = identref; sup = OPT binders_let ->
+ [ [ name = identref; sup = OPT binders ->
(let (loc,id) = name in (loc, Name id)),
(Option.default [] sup)
| -> (loc, Anonymous), [] ] ]
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index b0e4fc1f1..3cdf89ebd 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -354,10 +354,9 @@ module Constr =
let pattern = Gram.entry_create "constr:pattern"
let constr_pattern = gec_constr "constr_pattern"
let lconstr_pattern = gec_constr "lconstr_pattern"
- let binder = Gram.entry_create "constr:binder"
- let binder_let = Gram.entry_create "constr:binder_let"
- let binders_let = Gram.entry_create "constr:binders_let"
- let binders_let_fixannot = Gram.entry_create "constr:binders_let_fixannot"
+ let closed_binder = Gram.entry_create "constr:closed_binder"
+ let binders = Gram.entry_create "constr:binders"
+ let binders_fixannot = Gram.entry_create "constr:binders_fixannot"
let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint"
let record_declaration = Gram.entry_create "constr:record_declaration"
let appl_arg = Gram.entry_create "constr:appl_arg"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 1436b0e18..99c155e8d 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -196,10 +196,9 @@ module Constr :
val pattern : cases_pattern_expr Gram.entry
val constr_pattern : constr_expr Gram.entry
val lconstr_pattern : constr_expr Gram.entry
- val binder : (name located list * binder_kind * constr_expr) Gram.entry
- val binder_let : local_binder list Gram.entry
- val binders_let : local_binder list Gram.entry
- val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.entry
+ val closed_binder : local_binder list Gram.entry
+ val binders : local_binder list Gram.entry
+ val binders_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.entry
val typeclass_constraint : (name located * bool * constr_expr) Gram.entry
val record_declaration : constr_expr Gram.entry
val appl_arg : (constr_expr * explicitation located option) Gram.entry
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index e186dd76d..600ee3214 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -49,7 +49,7 @@ open Constr
let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
GEXTEND Gram
- GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder subtac_withtac;
+ GLOBAL: subtac_gallina_loc typeclass_constraint subtac_withtac;
subtac_gallina_loc:
[ [ g = Vernac.gallina -> loc, g
@@ -61,21 +61,12 @@ GEXTEND Gram
| -> None ] ]
;
- Constr.binder_let:
+ Constr.closed_binder:
[[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
[LocalRawAssum ([id], default_binder_kind, typ)]
] ];
- Constr.binder:
- [ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" ->
- ([id],default_binder_kind, mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, c, p)]))
- | "("; id=Prim.name; ":"; c=Constr.lconstr; ")" ->
- ([id],default_binder_kind, c)
- | "("; id=Prim.name; lid=LIST1 Prim.name; ":"; c=Constr.lconstr; ")" ->
- (id::lid,default_binder_kind, c)
- ] ];
-
END
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 18127593e..af9dac8df 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1279,12 +1279,12 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
(Ident (dummy_loc,id_of_string "Equivalence_Symmetric"), lemma2);
(Ident (dummy_loc,id_of_string "Equivalence_Transitive"), lemma3)])
-type 'a binders_let_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
+type 'a binders_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
-let (wit_binders_let : Genarg.tlevel binders_let_argtype),
- (globwit_binders_let : Genarg.glevel binders_let_argtype),
- (rawwit_binders_let : Genarg.rlevel binders_let_argtype) =
- Genarg.create_arg "binders_let"
+let (wit_binders : Genarg.tlevel binders_argtype),
+ (globwit_binders : Genarg.glevel binders_argtype),
+ (rawwit_binders : Genarg.rlevel binders_argtype) =
+ Genarg.create_arg "binders"
open Pcoq.Constr
@@ -1322,35 +1322,35 @@ VERNAC COMMAND EXTEND AddRelation3
END
VERNAC COMMAND EXTEND AddParametricRelation
- | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq)
+ | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
"reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
[ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None ]
- | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq)
+ | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
"reflexivity" "proved" "by" constr(lemma1)
"as" ident(n) ] ->
[ declare_relation ~binders:b a aeq n (Some lemma1) None None ]
- | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "as" ident(n) ] ->
+ | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] ->
[ declare_relation ~binders:b a aeq n None None None ]
END
VERNAC COMMAND EXTEND AddParametricRelation2
- [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+ [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
"as" ident(n) ] ->
[ declare_relation ~binders:b a aeq n None (Some lemma2) None ]
- | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
+ | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
[ declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) ]
END
VERNAC COMMAND EXTEND AddParametricRelation3
- [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
[ declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) ]
- | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
"as" ident(n) ] ->
[ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ]
- | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+ | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
"as" ident(n) ] ->
[ declare_relation ~binders:b a aeq n None None (Some lemma3) ]
END
@@ -1499,13 +1499,13 @@ let add_morphism glob binders m s n =
VERNAC COMMAND EXTEND AddSetoid1
[ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
[ add_setoid [] a aeq t n ]
- | [ "Add" "Parametric" "Setoid" binders_let(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+ | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
[ add_setoid binders a aeq t n ]
| [ "Add" "Morphism" constr(m) ":" ident(n) ] ->
[ add_morphism_infer (not (Vernacexpr.use_section_locality ())) m n ]
| [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] ->
[ add_morphism (not (Vernacexpr.use_section_locality ())) [] m s n ]
- | [ "Add" "Parametric" "Morphism" binders_let(binders) ":" constr(m)
+ | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
"with" "signature" lconstr(s) "as" ident(n) ] ->
[ add_morphism (not (Vernacexpr.use_section_locality ())) binders m s n ]
END
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-05 23:38:28 +0000