aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_vernac.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_vernac.ml4')
-rw-r--r--parsing/g_vernac.ml4182
1 files changed, 91 insertions, 91 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 0ebbaba92..4cd798e3e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -58,28 +58,28 @@ let get_command_entry () =
| Mode_none -> noedit_mode
let default_command_entry =
- Gram.Entry.of_parser "command_entry"
+ Gram.Entry.of_parser "command_entry"
(fun strm -> Gram.Entry.parse_token (get_command_entry ()) strm)
let no_hook _ _ = ()
GEXTEND Gram
GLOBAL: vernac gallina_ext tactic_mode proof_mode noedit_mode;
vernac: FIRST
- [ [ IDENT "Time"; v = vernac -> VernacTime v
+ [ [ IDENT "Time"; v = vernac -> VernacTime v
| IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
| locality; v = vernac_aux -> v ] ]
;
vernac_aux:
(* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
(* "." is still in the stream and discard_to_dot works correctly *)
- [ [ g = gallina; "." -> g
+ [ [ g = gallina; "." -> g
| g = gallina_ext; "." -> g
- | c = command; "." -> c
+ | c = command; "." -> c
| c = syntax; "." -> c
| "["; l = LIST1 located_vernac; "]"; "." -> VernacList l
] ]
;
- vernac_aux: LAST
+ vernac_aux: LAST
[ [ prfcom = default_command_entry -> prfcom ] ]
;
locality:
@@ -103,11 +103,11 @@ GEXTEND Gram
VernacSolve(g,tac,use_dft_tac)) ] ]
;
proof_mode:
- [ [ instr = proof_instr; "." -> VernacProofInstr instr ] ]
+ [ [ instr = proof_instr; "." -> VernacProofInstr instr ] ]
;
proof_mode: LAST
[ [ c=subgoal_command -> c (Some 1) ] ]
- ;
+ ;
located_vernac:
[ [ v = vernac -> loc, v ] ]
;
@@ -127,20 +127,20 @@ GEXTEND Gram
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
[ [ thm = thm_token; id = identref; bl = binders_let; ":"; c = lconstr;
- l = LIST0
+ l = LIST0
[ "with"; id = identref; bl = binders_let; ":"; c = lconstr ->
(Some id,(bl,c)) ] ->
VernacStartTheoremProof (thm,(Some id,(bl,c))::l, false, no_hook)
- | stre = assumption_token; nl = inline; bl = assum_list ->
+ | stre = assumption_token; nl = inline; bl = assum_list ->
VernacAssumption (stre, nl, bl)
| stre = assumptions_token; nl = inline; bl = assum_list ->
test_plurial_form bl;
VernacAssumption (stre, nl, bl)
- | IDENT "Boxed";"Definition";id = identref; b = def_body ->
+ | IDENT "Boxed";"Definition";id = identref; b = def_body ->
VernacDefinition ((Global,true,Definition), id, b, no_hook)
- | IDENT "Unboxed";"Definition";id = identref; b = def_body ->
+ | IDENT "Unboxed";"Definition";id = identref; b = def_body ->
VernacDefinition ((Global,false,Definition), id, b, no_hook)
- | (f,d) = def_token; id = identref; b = def_body ->
+ | (f,d) = def_token; id = identref; b = def_body ->
VernacDefinition (d, id, b, f)
(* Gallina inductive declarations *)
| f = finite_token;
@@ -157,12 +157,12 @@ GEXTEND Gram
| "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
VernacCoFixpoint (corecs,false)
| IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l
- | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
+ | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ]
;
gallina_ext:
[ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref;
- ps = binders_let;
+ ps = binders_let;
s = OPT [ ":"; s = lconstr -> s ];
cfs = [ ":="; l = constructor_list_or_record_decl -> l
| -> RecordDecl (None, []) ] ->
@@ -171,7 +171,7 @@ GEXTEND Gram
] ]
;
typeclass_context:
- [ [ "["; l=LIST1 typeclass_constraint SEP ","; "]" -> l
+ [ [ "["; l=LIST1 typeclass_constraint SEP ","; "]" -> l
| -> [] ] ]
;
thm_token:
@@ -184,14 +184,14 @@ GEXTEND Gram
| IDENT "Property" -> Property ] ]
;
def_token:
- [ [ "Definition" ->
+ [ [ "Definition" ->
no_hook, (Global, Flags.boxed_definitions(), Definition)
- | IDENT "Let" ->
+ | IDENT "Let" ->
no_hook, (Local, Flags.boxed_definitions(), Definition)
- | IDENT "Example" ->
+ | IDENT "Example" ->
no_hook, (Global, Flags.boxed_definitions(), Example)
| IDENT "SubClass" ->
- Class.add_subclass_hook, (use_locality_exp (), false, SubClass) ] ]
+ Class.add_subclass_hook, (use_locality_exp (), false, SubClass) ] ]
;
assumption_token:
[ [ "Hypothesis" -> (Local, Logical)
@@ -218,7 +218,7 @@ GEXTEND Gram
;
record_token:
[ [ IDENT "Record" -> (Record,BiFinite)
- | IDENT "Structure" -> (Structure,BiFinite)
+ | IDENT "Structure" -> (Structure,BiFinite)
| IDENT "Class" -> (Class true,BiFinite) ] ]
;
(* Simple definitions *)
@@ -237,24 +237,24 @@ GEXTEND Gram
| -> None ] ]
;
decl_notation:
- [ [ OPT [ "where"; ntn = ne_string; ":="; c = constr;
+ [ [ OPT [ "where"; ntn = ne_string; ":="; c = constr;
scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ] ]
;
(* Inductives and records *)
inductive_definition:
- [ [ id = identref; oc = opt_coercion; indpar = binders_let;
+ [ [ id = identref; oc = opt_coercion; indpar = binders_let;
c = OPT [ ":"; c = lconstr -> c ];
":="; lc = constructor_list_or_record_decl; ntn = decl_notation ->
(((oc,id),indpar,c,lc),ntn) ] ]
;
constructor_list_or_record_decl:
[ [ "|"; l = LIST1 constructor SEP "|" -> Constructors l
- | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" ->
+ | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" ->
Constructors ((c id)::l)
| id = identref ; c = constructor_type -> Constructors [ c id ]
- | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" ->
- RecordDecl (Some cstr,fs)
- | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs)
+ | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" ->
+ RecordDecl (Some cstr,fs)
+ | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs)
| -> Constructors [] ] ]
;
(*
@@ -268,9 +268,9 @@ GEXTEND Gram
;
(* (co)-fixpoints *)
rec_definition:
- [ [ id = identref;
+ [ [ id = identref;
bl = binders_let_fixannot;
- ty = type_cstr;
+ ty = type_cstr;
":="; def = lconstr; ntn = decl_notation ->
let bl, annot = bl in
let names = names_of_local_assums bl in
@@ -282,13 +282,13 @@ GEXTEND Gram
else Util.user_err_loc
(loc,"Fixpoint",
str "No argument named " ++ Nameops.pr_id id ++ str"."))
- | None ->
- (* If there is only one argument, it is the recursive one,
+ | None ->
+ (* If there is only one argument, it is the recursive one,
otherwise, we search the recursive index later *)
match names with
| [(loc, Name na)] -> Some (loc, na)
- | _ -> None
- in
+ | _ -> None
+ in
((id,(ni,snd annot),bl,ty,def),ntn) ] ]
;
corec_definition:
@@ -297,7 +297,7 @@ GEXTEND Gram
((id,bl,ty,def),ntn) ] ]
;
type_cstr:
- [ [ ":"; c=lconstr -> c
+ [ [ ":"; c=lconstr -> c
| -> CHole (loc, None) ] ]
;
(* Inductive schemes *)
@@ -329,7 +329,7 @@ GEXTEND Gram
[ [ bd = record_binder; ntn = decl_notation -> bd,ntn ] ]
;
record_binder_body:
- [ [ l = binders_let; oc = of_type_with_opt_coercion;
+ [ [ l = binders_let; 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;
t = lconstr; ":="; b = lconstr -> fun id ->
@@ -352,12 +352,12 @@ GEXTEND Gram
[ [ "("; a = simple_assum_coe; ")" -> a ] ]
;
simple_assum_coe:
- [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr ->
+ [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr ->
(oc,(idl,c)) ] ]
;
constructor_type:
- [[ l = binders_let;
+ [[ l = binders_let;
t= [ coe = of_type_with_opt_coercion; c = lconstr ->
fun l id -> (coe,(id,mkCProdN loc l c))
| ->
@@ -383,16 +383,16 @@ GEXTEND Gram
gallina_ext:
[ [ (* Interactive module declaration *)
- IDENT "Module"; export = export_token; id = identref;
- bl = LIST0 module_binder; mty_o = OPT of_module_type;
+ IDENT "Module"; export = export_token; id = identref;
+ bl = LIST0 module_binder; mty_o = OPT of_module_type;
mexpr_o = OPT is_module_expr ->
VernacDefineModule (export, id, bl, mty_o, mexpr_o)
-
- | IDENT "Module"; "Type"; id = identref;
+
+ | IDENT "Module"; "Type"; id = identref;
bl = LIST0 module_binder; mty_o = OPT is_module_type ->
VernacDeclareModuleType (id, bl, mty_o)
-
- | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref;
+
+ | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref;
bl = LIST0 module_binder; ":"; mty = module_type ->
VernacDeclareModule (export, id, bl, (mty,true))
(* Section beginning *)
@@ -405,10 +405,10 @@ GEXTEND Gram
(* Requiring an already compiled module *)
| IDENT "Require"; export = export_token; qidl = LIST1 global ->
VernacRequire (export, None, qidl)
- | IDENT "Require"; export = export_token; filename = ne_string ->
+ | IDENT "Require"; export = export_token; filename = ne_string ->
VernacRequireFrom (export, None, filename)
| IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
- | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl)
+ | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl)
| IDENT "Include"; expr = module_expr -> VernacInclude(CIME(expr))
| IDENT "Include"; "Type"; expr = module_type -> VernacInclude(CIMTE(expr)) ] ]
;
@@ -418,7 +418,7 @@ GEXTEND Gram
| -> None ] ]
;
of_module_type:
- [ [ ":"; mty = module_type -> (mty, true)
+ [ [ ":"; mty = module_type -> (mty, true)
| "<:"; mty = module_type -> (mty, false) ] ]
;
is_module_type:
@@ -453,13 +453,13 @@ GEXTEND Gram
module_type:
[ [ qid = qualid -> CMTEident qid
(* ... *)
- | mty = module_type; me = module_expr_atom -> CMTEapply (mty,me)
+ | mty = module_type; me = module_expr_atom -> CMTEapply (mty,me)
| mty = module_type; "with"; decl = with_declaration -> CMTEwith (mty,decl)
] ]
;
END
-(* Extensions: implicits, coercions, etc. *)
+(* Extensions: implicits, coercions, etc. *)
GEXTEND Gram
GLOBAL: gallina_ext;
@@ -480,7 +480,7 @@ GEXTEND Gram
| IDENT "Canonical"; IDENT "Structure"; qid = global;
d = def_body ->
let s = coerce_reference_to_id qid in
- VernacDefinition
+ VernacDefinition
((Global,false,CanonicalStructure),(dummy_loc,s),d,
(fun _ -> Recordops.declare_canonical_structure))
@@ -492,16 +492,16 @@ GEXTEND Gram
let s = coerce_reference_to_id qid in
VernacDefinition ((enforce_locality_exp (),false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
| IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
- ":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
+ ":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
VernacIdentityCoercion (enforce_locality_exp (), f, s, t)
| IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
- s = class_rawexpr; ">->"; t = class_rawexpr ->
+ s = class_rawexpr; ">->"; t = class_rawexpr ->
VernacIdentityCoercion (use_locality_exp (), f, s, t)
| IDENT "Coercion"; IDENT "Local"; qid = global; ":";
- s = class_rawexpr; ">->"; t = class_rawexpr ->
+ s = class_rawexpr; ">->"; t = class_rawexpr ->
VernacCoercion (enforce_locality_exp (), AN qid, s, t)
| IDENT "Coercion"; IDENT "Local"; ntn = by_notation; ":";
- s = class_rawexpr; ">->"; t = class_rawexpr ->
+ s = class_rawexpr; ">->"; t = class_rawexpr ->
VernacCoercion (enforce_locality_exp (), ByNotation ntn, s, t)
| IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
t = class_rawexpr ->
@@ -509,29 +509,29 @@ GEXTEND Gram
| IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->";
t = class_rawexpr ->
VernacCoercion (use_locality_exp (), ByNotation ntn, s, t)
-
- | IDENT "Context"; c = binders_let ->
+
+ | IDENT "Context"; c = binders_let ->
VernacContext c
-
+
| IDENT "Instance"; ":";
expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
- pri = OPT [ "|"; i = natural -> i ] ;
- props = [ ":="; "{"; r = record_declaration; "}" -> r |
+ pri = OPT [ "|"; i = natural -> i ] ;
+ props = [ ":="; "{"; r = record_declaration; "}" -> r |
":="; c = lconstr -> c | -> CRecord (loc, None, []) ] ->
VernacInstance (not (use_non_locality ()), [], ((loc,Anonymous), expl, t), props, pri)
| IDENT "Instance"; name = identref; sup = OPT binders_let; ":";
expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
- pri = OPT [ "|"; i = natural -> i ] ;
- props = [ ":="; "{"; r = record_declaration; "}" -> r |
+ pri = OPT [ "|"; i = natural -> i ] ;
+ props = [ ":="; "{"; r = record_declaration; "}" -> r |
":="; c = lconstr -> c | -> CRecord (loc, None, []) ] ->
let sup =
match sup with
None -> []
| Some l -> l
in
- let n =
- let (loc, id) = name in
+ let n =
+ let (loc, id) = name in
(loc, Name id)
in
VernacInstance (not (use_non_locality ()), sup, (n, expl, t), props, pri)
@@ -539,8 +539,8 @@ GEXTEND Gram
| IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is
(* Implicit *)
- | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global;
- pos = OPT [ "["; l = LIST0 implicit_name; "]" ->
+ | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global;
+ pos = OPT [ "["; l = LIST0 implicit_name; "]" ->
List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
VernacDeclareImplicits (use_section_locality (),qid,pos)
@@ -550,7 +550,7 @@ GEXTEND Gram
implicit_name:
[ [ "!"; id = ident -> (id, false, true)
| id = ident -> (id,false,false)
- | "["; "!"; id = ident; "]" -> (id,true,true)
+ | "["; "!"; id = ident; "]" -> (id,true,true)
| "["; id = ident; "]" -> (id,true, false) ] ]
;
strategy_level:
@@ -592,7 +592,7 @@ GEXTEND Gram
(* Managing load paths *)
| IDENT "Add"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath ->
VernacAddLoadPath (false, dir, alias)
- | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string;
+ | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string;
alias = as_dirpath -> VernacAddLoadPath (true, dir, alias)
| IDENT "Remove"; IDENT "LoadPath"; dir = ne_string ->
VernacRemoveLoadPath dir
@@ -611,23 +611,23 @@ GEXTEND Gram
(* Printing (careful factorization of entries) *)
| IDENT "Print"; p = printable -> VernacPrint p
| IDENT "Print"; qid = smart_global -> VernacPrint (PrintName qid)
- | IDENT "Print"; IDENT "Module"; "Type"; qid = global ->
+ | IDENT "Print"; IDENT "Module"; "Type"; qid = global ->
VernacPrint (PrintModuleType qid)
- | IDENT "Print"; IDENT "Module"; qid = global ->
+ | IDENT "Print"; IDENT "Module"; qid = global ->
VernacPrint (PrintModule qid)
| IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n)
| IDENT "About"; qid = smart_global -> VernacPrint (PrintAbout qid)
(* Searching the environment *)
- | IDENT "Search"; c = constr_pattern; l = in_or_out_modules ->
+ | IDENT "Search"; c = constr_pattern; l = in_or_out_modules ->
VernacSearch (SearchHead c, l)
| IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules ->
VernacSearch (SearchPattern c, l)
| IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules ->
VernacSearch (SearchRewrite c, l)
- | IDENT "SearchAbout";
+ | IDENT "SearchAbout";
sl = [ "[";
- l = LIST1 [
+ l = LIST1 [
b = positive_search_mark; s = ne_string; sc = OPT scope
-> b, SearchString (s,sc)
| b = positive_search_mark; p = constr_pattern
@@ -635,7 +635,7 @@ GEXTEND Gram
]; "]" -> l
| p = constr_pattern -> [true,SearchSubPattern p]
| s = ne_string; sc = OPT scope -> [true,SearchString (s,sc)] ];
- l = in_or_out_modules ->
+ l = in_or_out_modules ->
VernacSearch (SearchAbout sl, l)
| IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
@@ -671,7 +671,7 @@ GEXTEND Gram
| IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value
-> VernacRemoveOption ([table;field], v)
| IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value ->
- VernacRemoveOption ([table], v)
+ VernacRemoveOption ([table], v)
| IDENT "proof" -> VernacDeclProof
| "return" -> VernacReturn ]]
@@ -690,7 +690,7 @@ GEXTEND Gram
(* This should be in "syntax" section but is here for factorization*)
PrintGrammar ent
| IDENT "LoadPath"; dir = OPT dirpath -> PrintLoadPath dir
- | IDENT "Modules" ->
+ | IDENT "Modules" ->
error "Print Modules is obsolete; use Print Libraries instead"
| IDENT "Libraries" -> PrintModules
@@ -764,7 +764,7 @@ END;
GEXTEND Gram
command:
- [ [
+ [ [
(* State management *)
IDENT "Write"; IDENT "State"; s = IDENT -> VernacWriteState s
| IDENT "Write"; IDENT "State"; s = ne_string -> VernacWriteState s
@@ -778,11 +778,11 @@ GEXTEND Gram
| IDENT "Back" -> VernacBack 1
| IDENT "Back"; n = natural -> VernacBack n
| IDENT "BackTo"; n = natural -> VernacBackTo n
- | IDENT "Backtrack"; n = natural ; m = natural ; p = natural ->
+ | IDENT "Backtrack"; n = natural ; m = natural ; p = natural ->
VernacBacktrack (n,m,p)
(* Tactic Debugger *)
- | IDENT "Debug"; IDENT "On" ->
+ | IDENT "Debug"; IDENT "On" ->
VernacSetOption (None,["Ltac";"Debug"], BoolValue true)
| IDENT "Debug"; IDENT "Off" ->
@@ -798,38 +798,38 @@ GEXTEND Gram
GLOBAL: syntax;
syntax:
- [ [ IDENT "Open"; local = obsolete_locality; IDENT "Scope"; sc = IDENT ->
+ [ [ IDENT "Open"; local = obsolete_locality; IDENT "Scope"; sc = IDENT ->
VernacOpenCloseScope (enforce_locality_of local,true,sc)
- | IDENT "Close"; local = obsolete_locality; IDENT "Scope"; sc = IDENT ->
+ | IDENT "Close"; local = obsolete_locality; IDENT "Scope"; sc = IDENT ->
VernacOpenCloseScope (enforce_locality_of local,false,sc)
| IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
VernacDelimiters (sc,key)
- | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
+ | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
| IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
- "["; scl = LIST0 opt_scope; "]" ->
+ "["; scl = LIST0 opt_scope; "]" ->
VernacArgumentsScope (use_non_locality (),qid,scl)
| IDENT "Infix"; local = obsolete_locality;
- op = ne_string; ":="; p = constr;
+ op = ne_string; ":="; p = constr;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc ] ->
VernacInfix (enforce_locality_of local,(op,modl),p,sc)
- | IDENT "Notation"; local = obsolete_locality; id = identref;
+ | IDENT "Notation"; local = obsolete_locality; id = identref;
idl = LIST0 ident; ":="; c = constr;
b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] ->
VernacSyntacticDefinition (id,(idl,c),enforce_locality_of local,b)
- | IDENT "Notation"; local = obsolete_locality; s = ne_string; ":=";
+ | IDENT "Notation"; local = obsolete_locality; s = ne_string; ":=";
c = constr;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc ] ->
VernacNotation (enforce_locality_of local,c,(s,modl),sc)
- | IDENT "Tactic"; IDENT "Notation"; n = tactic_level;
+ | IDENT "Tactic"; IDENT "Notation"; n = tactic_level;
pil = LIST1 production_item; ":="; t = Tactic.tactic
-> VernacTacticNotation (n,pil,t)
@@ -838,12 +838,12 @@ GEXTEND Gram
Metasyntax.check_infix_modifiers l;
VernacSyntaxExtension (use_locality (),("x '"^s^"' y",l))
- | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality;
- s = ne_string;
+ | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality;
+ s = ne_string;
l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
-> VernacSyntaxExtension (enforce_locality_of local,(s,l))
- (* "Print" "Grammar" should be here but is in "command" entry in order
+ (* "Print" "Grammar" should be here but is in "command" entry in order
to factorize with other "Print"-based vernac entries *)
] ]
;
@@ -859,7 +859,7 @@ GEXTEND Gram
;
syntax_modifier:
[ [ x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev)
- | x = IDENT; ","; l = LIST1 IDENT SEP ","; "at";
+ | x = IDENT; ","; l = LIST1 IDENT SEP ","; "at";
lev = level -> SetItemLevel (x::l,lev)
| "at"; IDENT "level"; n = natural -> SetLevel n
| IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA
@@ -871,7 +871,7 @@ GEXTEND Gram
;
syntax_extension_type:
[ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference
- | IDENT "bigint" -> ETBigint
+ | IDENT "bigint" -> ETBigint
] ]
;
opt_scope:
@@ -879,8 +879,8 @@ GEXTEND Gram
;
production_item:
[ [ s = ne_string -> TacTerm s
- | nt = IDENT;
- po = OPT [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ];
+ | nt = IDENT;
+ po = OPT [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ];
")" -> (p,sep) ] -> TacNonTerm (loc,nt,po) ] ]
;
END
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 17:10:57 +0000