diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 337 |
1 files changed, 176 insertions, 161 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 839f768b..e61be53a 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -8,7 +8,7 @@ open Pp open Compat -open Errors +open CErrors open Util open Names open Constrexpr @@ -20,22 +20,19 @@ open Misctypes open Tok (* necessary for camlp4 *) open Pcoq -open Pcoq.Tactic open Pcoq.Prim open Pcoq.Constr open Pcoq.Vernac_ open Pcoq.Module let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ] -let _ = List.iter Lexer.add_keyword vernac_kw +let _ = List.iter CLexer.add_keyword vernac_kw (* Rem: do not join the different GEXTEND into one, it breaks native *) (* compilation on PowerPC and Sun architectures *) let query_command = Gram.entry_create "vernac:query_command" -let tactic_mode = Gram.entry_create "vernac:tactic_command" -let noedit_mode = Gram.entry_create "vernac:noedit_command" let subprf = Gram.entry_create "vernac:subprf" let class_rawexpr = Gram.entry_create "vernac:class_rawexpr" @@ -48,21 +45,6 @@ let subgoal_command = Gram.entry_create "proof_mode:subgoal_command" let instance_name = Gram.entry_create "vernac:instance_name" let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" -let command_entry = ref noedit_mode -let set_command_entry e = command_entry := e -let get_command_entry () = !command_entry - - -(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for - proof editing and changes nothing else). Then sets it as the default proof mode. *) -let set_tactic_mode () = set_command_entry tactic_mode -let set_noedit_mode () = set_command_entry noedit_mode -let _ = Proof_global.register_proof_mode {Proof_global. - name = "Classic" ; - set = set_tactic_mode ; - reset = set_noedit_mode - } - let make_bullet s = let n = String.length s in match s.[0] with @@ -71,26 +53,11 @@ let make_bullet s = | '*' -> Star n | _ -> assert false -(* Hack to parse "[ id" without dropping [ *) -let test_bracket_ident = - Gram.Entry.of_parser "test_bracket_ident" - (fun strm -> - match get_tok (stream_nth 0 strm) with - | KEYWORD "[" -> - (match get_tok (stream_nth 1 strm) with - | IDENT _ -> () - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) - -let default_command_entry = - Gram.Entry.of_parser "command_entry" - (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm) - GEXTEND Gram - GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command; + GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command; vernac: FIRST - [ [ IDENT "Time"; l = vernac_list -> VernacTime l - | IDENT "Redirect"; s = ne_string; l = vernac_list -> VernacRedirect (s, l) + [ [ IDENT "Time"; c = located_vernac -> VernacTime c + | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c) | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) | IDENT "Fail"; v = vernac -> VernacFail v @@ -128,28 +95,13 @@ GEXTEND Gram | c = subprf -> c ] ] ; - vernac_list: - [ [ c = located_vernac -> [c] ] ] - ; vernac_aux: LAST - [ [ prfcom = default_command_entry -> prfcom ] ] + [ [ prfcom = command_entry -> prfcom ] ] ; noedit_mode: [ [ c = subgoal_command -> c None] ] ; - selector: - [ [ n=natural; ":" -> SelectNth n - | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id - | IDENT "all" ; ":" -> SelectAll - | IDENT "par" ; ":" -> SelectAllParallel ] ] - ; - - tactic_mode: - [ [ gln = OPT selector; - tac = subgoal_command -> tac gln ] ] - ; - subprf: [ [ s = BULLET -> VernacBullet (make_bullet s) | "{" -> VernacSubproof None @@ -164,35 +116,37 @@ GEXTEND Gram | None -> c None | _ -> VernacError (UserError ("",str"Typing and evaluation commands, cannot be used with the \"all:\" selector.")) - end - | info = OPT [IDENT "Info";n=natural -> n]; - tac = Tactic.tactic; - use_dft_tac = [ "." -> false | "..." -> true ] -> - (fun g -> - let g = Option.default (Proof_global.get_default_goal_selector ()) g in - VernacSolve(g,info,tac,use_dft_tac)) ] ] + end ] ] ; located_vernac: [ [ v = vernac -> !@loc, v ] ] ; END -let test_plurial_form = function +let warn_plural_command = + CWarnings.create ~name:"plural-command" ~category:"pedantic" ~default:CWarnings.Disabled + (fun kwd -> strbrk (Printf.sprintf "Command \"%s\" expects more than one assumption." kwd)) + +let test_plural_form loc kwd = function | [(_,([_],_))] -> - Flags.if_verbose msg_warning - (strbrk "Keywords Variables/Hypotheses/Parameters expect more than one assumption") + warn_plural_command ~loc:!@loc kwd | _ -> () -let test_plurial_form_types = function +let test_plural_form_types loc kwd = function | [([_],_)] -> - Flags.if_verbose msg_warning - (strbrk "Keywords Implicit Types expect more than one type") + warn_plural_command ~loc:!@loc kwd | _ -> () +let fresh_var env c = + Namegen.next_ident_away (Id.of_string "pat") + (env @ Id.Set.elements (Topconstr.free_vars_of_constr_expr c)) + +let _ = Hook.set Constrexpr_ops.fresh_var_hook fresh_var + (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - record_field decl_notation rec_definition; + record_field decl_notation rec_definition pidentref; gallina: (* Definition, Theorem, Variable, Axiom, ... *) @@ -203,8 +157,8 @@ GEXTEND Gram VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false) | stre = assumption_token; nl = inline; bl = assum_list -> VernacAssumption (stre, nl, bl) - | stre = assumptions_token; nl = inline; bl = assum_list -> - test_plurial_form bl; + | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list -> + test_plural_form loc kwd bl; VernacAssumption (stre, nl, bl) | d = def_token; id = pidentref; b = def_body -> VernacDefinition (d, id, b) @@ -257,11 +211,11 @@ GEXTEND Gram | IDENT "Conjecture" -> (None, Conjectural) ] ] ; assumptions_token: - [ [ IDENT "Hypotheses" -> (Some Discharge, Logical) - | IDENT "Variables" -> (Some Discharge, Definitional) - | IDENT "Axioms" -> (None, Logical) - | IDENT "Parameters" -> (None, Definitional) - | IDENT "Conjectures" -> (None, Conjectural) ] ] + [ [ IDENT "Hypotheses" -> ("Hypotheses", (Some Discharge, Logical)) + | IDENT "Variables" -> ("Variables", (Some Discharge, Definitional)) + | IDENT "Axioms" -> ("Axioms", (None, Logical)) + | IDENT "Parameters" -> ("Parameters", (None, Definitional)) + | IDENT "Conjectures" -> ("Conjectures", (None, Conjectural)) ] ] ; inline: [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i) @@ -272,8 +226,8 @@ GEXTEND Gram [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ] ; univ_constraint: - [ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; - r = identref -> (l, ord, r) ] ] + [ [ l = universe_level; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; + r = universe_level -> (l, ord, r) ] ] ; finite_token: [ [ "Inductive" -> (Inductive_kw,Finite) @@ -289,11 +243,19 @@ GEXTEND Gram (* Simple definitions *) def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> + let (bl, c) = expand_pattern_binders mkCLambdaN bl c in (match c with CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> - DefineBody (bl, red, c, Some t) + let ((bl, c), tyo) = + if List.exists (function LocalPattern _ -> true | _ -> false) bl + then + let c = CCast (!@loc, c, CastConv t) in + (expand_pattern_binders mkCLambdaN bl c, None) + else ((bl, c), Some t) + in + DefineBody (bl, red, c, tyo) | bl = binders; ":"; t = lconstr -> ProveBody (bl, t) ] ] ; @@ -462,6 +424,10 @@ let starredidentreflist_to_expr l = | [] -> SsEmpty | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x +let warn_deprecated_include_type = + CWarnings.create ~name:"deprecated-include-type" ~category:"deprecated" + (fun () -> strbrk "Include Type is deprecated; use Include instead") + (* Modules and Sections *) GEXTEND Gram GLOBAL: gallina_ext module_expr module_type section_subset_expr; @@ -501,9 +467,8 @@ GEXTEND Gram | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr -> VernacInclude(e::l) | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type -> - Flags.if_verbose - msg_warning (strbrk "Include Type is deprecated; use Include instead"); - VernacInclude(e::l) ] ] + warn_deprecated_include_type ~loc:!@loc (); + VernacInclude(e::l) ] ] ; export_token: [ [ IDENT "Import" -> Some false @@ -607,9 +572,23 @@ GEXTEND Gram ; END +let warn_deprecated_arguments_scope = + CWarnings.create ~name:"deprecated-arguments-scope" ~category:"deprecated" + (fun () -> strbrk "Arguments Scope is deprecated; use Arguments instead") + +let warn_deprecated_implicit_arguments = + CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated" + (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead") + +let warn_deprecated_arguments_syntax = + CWarnings.create ~name:"deprecated-arguments-syntax" ~category:"deprecated" + (fun () -> strbrk "The \"/\" and \"!\" modifiers have an effect only " + ++ strbrk "in the first arguments list. The syntax allowing" + ++ strbrk " them to appear in other lists is deprecated.") + (* Extensions: implicits, coercions, etc. *) GEXTEND Gram - GLOBAL: gallina_ext instance_name; + GLOBAL: gallina_ext instance_name hint_info; gallina_ext: [ [ (* Transparent and Opaque *) @@ -662,81 +641,69 @@ GEXTEND Gram | IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; - pri = OPT [ "|"; i = natural -> i ] ; + info = hint_info ; props = [ ":="; "{"; r = record_declaration; "}" -> Some (true,r) | ":="; c = lconstr -> Some (false,c) | -> None ] -> - VernacInstance (false,snd namesup,(fst namesup,expl,t),props,pri) + VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info) | IDENT "Existing"; IDENT "Instance"; id = global; - pri = OPT [ "|"; i = natural -> i ] -> - VernacDeclareInstances ([id], pri) + info = hint_info -> + VernacDeclareInstances [id, info] + | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global; - pri = OPT [ "|"; i = natural -> i ] -> - VernacDeclareInstances (ids, pri) + pri = OPT [ "|"; i = natural -> i ] -> + let info = { hint_priority = pri; hint_pattern = None } in + let insts = List.map (fun i -> (i, info)) ids in + VernacDeclareInstances insts | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is (* Arguments *) | IDENT "Arguments"; qid = smart_global; - impl = LIST1 [ l = LIST0 - [ item = argument_spec -> - let id, r, s = item in [`Id (id,r,s,false,false)] - | "/" -> [`Slash] - | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> - let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x - | Some _, Some _ -> error "scope declared twice" in - List.map (fun (id,r,s) -> `Id(id,r,f s,false,false)) items - | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> - let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x - | Some _, Some _ -> error "scope declared twice" in - List.map (fun (id,r,s) -> `Id(id,r,f s,true,false)) items - | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> - let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x - | Some _, Some _ -> error "scope declared twice" in - List.map (fun (id,r,s) -> `Id(id,r,f s,true,true)) items - ] -> l ] SEP ","; + args = LIST0 argument_spec_block; + more_implicits = OPT + [ ","; impl = LIST1 + [ impl = LIST0 more_implicits_block -> + let warn_deprecated = List.exists fst impl in + if warn_deprecated then warn_deprecated_arguments_syntax ~loc:!@loc (); + List.flatten (List.map snd impl)] + SEP "," -> impl + ]; mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] -> let mods = match mods with None -> [] | Some l -> List.flatten l in - let impl = List.map List.flatten impl in - let rec aux n (narg, impl) = function - | `Id x :: tl -> aux (n+1) (narg, impl@[x]) tl - | `Slash :: tl -> aux (n+1) (n, impl) tl - | [] -> narg, impl in - let nargs, impl = List.split (List.map (aux 0 (-1, [])) impl) in - let nargs, rest = List.hd nargs, List.tl nargs in - if List.exists (fun arg -> not (Int.equal arg nargs)) rest then - error "All arguments lists must have the same length"; - let err_incompat x y = - error ("Options \""^x^"\" and \""^y^"\" are incompatible") in - if nargs > 0 && List.mem `ReductionNeverUnfold mods then - err_incompat "simpl never" "/"; - if List.mem `ReductionNeverUnfold mods && - List.mem `ReductionDontExposeCase mods then - err_incompat "simpl never" "simpl nomatch"; - VernacArguments (qid, impl, nargs, mods) - + let slash_position = ref None in + let rec parse_args i = function + | [] -> [] + | `Id x :: args -> x :: parse_args (i+1) args + | `Slash :: args -> + if Option.is_empty !slash_position then + (slash_position := Some i; parse_args i args) + else + error "The \"/\" modifier can occur only once" + in + let args = parse_args 0 (List.flatten args) in + let more_implicits = Option.default [] more_implicits in + VernacArguments (qid, args, more_implicits, !slash_position, mods) + + (* moved there so that camlp5 factors it with the previous rule *) | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> - msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead"); + warn_deprecated_arguments_scope ~loc:!@loc (); VernacArgumentsScope (qid,scl) (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; pos = LIST0 [ "["; l = LIST0 implicit_name; "]" -> List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> - Flags.if_verbose - msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead"); - VernacDeclareImplicits (qid,pos) + warn_deprecated_implicit_arguments ~loc:!@loc (); + VernacDeclareImplicits (qid,pos) | IDENT "Implicit"; "Type"; bl = reserv_list -> VernacReserve bl | IDENT "Implicit"; IDENT "Types"; bl = reserv_list -> - test_plurial_form_types bl; + test_plural_form_types loc "Implicit Types" bl; VernacReserve bl | IDENT "Generalizable"; @@ -775,6 +742,55 @@ GEXTEND Gram snd id, not (Option.is_empty b), Option.map (fun x -> !@loc, x) s ] ]; + (* List of arguments implicit status, scope, modifiers *) + argument_spec_block: [ + [ item = argument_spec -> + let name, recarg_like, notation_scope = item in + [`Id { name=name; recarg_like=recarg_like; + notation_scope=notation_scope; + implicit_status = NotImplicit}] + | "/" -> [`Slash] + | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> + let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x + | Some _, Some _ -> error "scope declared twice" in + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = NotImplicit}) items + | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> + let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x + | Some _, Some _ -> error "scope declared twice" in + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = Implicit}) items + | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> + let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x + | Some _, Some _ -> error "scope declared twice" in + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = MaximallyImplicit}) items + ] + ]; + name_or_bang: [ + [ b = OPT "!"; id = name -> + not (Option.is_empty b), id + ] + ]; + (* Same as [argument_spec_block], but with only implicit status and names *) + more_implicits_block: [ + [ (bang,name) = name_or_bang -> (bang, [(snd name, Vernacexpr.NotImplicit)]) + | "/" -> (true (* Should warn about deprecated syntax *), []) + | "["; items = LIST1 name_or_bang; "]" -> + (List.exists fst items, List.map (fun (_,(_,name)) -> (name, Vernacexpr.Implicit)) items) + | "{"; items = LIST1 name_or_bang; "}" -> + (List.exists fst items, List.map (fun (_,(_,name)) -> (name, Vernacexpr.MaximallyImplicit)) items) + ] + ]; strategy_level: [ [ IDENT "expand" -> Conv_oracle.Expand | IDENT "opaque" -> Conv_oracle.Opaque @@ -783,10 +799,15 @@ GEXTEND Gram | IDENT "transparent" -> Conv_oracle.transparent ] ] ; instance_name: - [ [ name = identref; sup = OPT binders -> - (let (loc,id) = name in (loc, Name id)), + [ [ name = pidentref; sup = OPT binders -> + (let ((loc,id),l) = name in ((loc, Name id),l)), (Option.default [] sup) - | -> (!@loc, Anonymous), [] ] ] + | -> ((!@loc, Anonymous), None), [] ] ] + ; + hint_info: + [ [ "|"; i = OPT natural; pat = OPT constr_pattern -> + { hint_priority = i; hint_pattern = pat } + | -> { hint_priority = None; hint_pattern = None } ] ] ; reserv_list: [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ] @@ -804,17 +825,13 @@ GEXTEND Gram GLOBAL: command query_command class_rawexpr; command: - [ [ IDENT "Ltac"; - l = LIST1 tacdef_body SEP "with" -> - VernacDeclareTacticDefinition (true, l) - - | IDENT "Comments"; l = LIST0 comment -> VernacComments l + [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l (* Hack! Should be in grammar_ext, but camlp4 factorize badly *) | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; - pri = OPT [ "|"; i = natural -> i ] -> - VernacInstance (true, snd namesup, (fst namesup, expl, t), None, pri) + info = hint_info -> + VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) (* System directory *) | IDENT "Pwd" -> VernacChdir None @@ -870,7 +887,20 @@ GEXTEND Gram (* For acting on parameter tables *) | "Set"; table = option_table; v = option_value -> - VernacSetOption (table,v) + begin match v with + | StringValue s -> + (* We make a special case for warnings because appending is their + natural semantics *) + if CString.List.equal table ["Warnings"] then + VernacSetAppendOption (table, s) + else + let (last, prefix) = List.sep_last table in + if String.equal last "Append" && not (List.is_empty prefix) then + VernacSetAppendOption (prefix, s) + else + VernacSetOption (table, v) + | _ -> VernacSetOption (table, v) + end | "Set"; table = option_table -> VernacSetOption (table,BoolValue true) | IDENT "Unset"; table = option_table -> @@ -943,7 +973,6 @@ GEXTEND Gram | IDENT "Classes" -> PrintClasses | IDENT "TypeClasses" -> PrintTypeClasses | IDENT "Instances"; qid = smart_global -> PrintInstances qid - | IDENT "Ltac"; qid = global -> PrintLtac qid | IDENT "Coercions" -> PrintCoercions | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> PrintCoercionPaths (s,t) @@ -954,7 +983,6 @@ GEXTEND Gram | IDENT "Hint"; qid = smart_global -> PrintHint qid | IDENT "Hint"; "*" -> PrintHintDb | IDENT "HintDb"; s = IDENT -> PrintHintDbName s - | "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s | IDENT "Scopes" -> PrintScopes | IDENT "Scope"; s = IDENT -> PrintScope s | IDENT "Visibility"; s = OPT [x = IDENT -> x ] -> PrintVisibility s @@ -1083,7 +1111,7 @@ GEXTEND Gram VernacDelimiters (sc, None) | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; - refl = LIST1 smart_global -> VernacBindScope (sc,refl) + refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl) | IDENT "Infix"; local = obsolete_locality; op = ne_lstring; ":="; p = constr; @@ -1102,10 +1130,6 @@ GEXTEND Gram | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING -> VernacNotationAddFormat (n,s,fmt) - | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; - pil = LIST1 production_item; ":="; t = Tactic.tactic - -> VernacTacticNotation (n,pil,t) - | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> Metasyntax.check_infix_modifiers l; @@ -1131,9 +1155,6 @@ GEXTEND Gram obsolete_locality: [ [ IDENT "Local" -> true | -> false ] ] ; - tactic_level: - [ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ] - ; level: [ [ IDENT "level"; n = natural -> NumLevel n | IDENT "next"; IDENT "level" -> NextLevel ] ] @@ -1143,10 +1164,10 @@ GEXTEND Gram | IDENT "left"; IDENT "associativity" -> SetAssoc LeftA | IDENT "right"; IDENT "associativity" -> SetAssoc RightA | IDENT "no"; IDENT "associativity" -> SetAssoc NonA - | IDENT "only"; IDENT "parsing" -> - SetOnlyParsing Flags.Current + | IDENT "only"; IDENT "printing" -> SetOnlyPrinting + | IDENT "only"; IDENT "parsing" -> SetOnlyParsing | IDENT "compat"; s = STRING -> - SetOnlyParsing (Coqinit.get_compat_version s) + SetCompatVersion (Coqinit.get_compat_version s) | IDENT "format"; s1 = [s = STRING -> (!@loc,s)]; s2 = OPT [s = STRING -> (!@loc,s)] -> begin match s1, s2 with @@ -1165,10 +1186,4 @@ GEXTEND Gram | IDENT "closed"; IDENT "binder" -> ETBinder false ] ] ; - production_item: - [ [ s = ne_string -> TacTerm s - | nt = IDENT; - po = OPT [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ]; - ")" -> (p,sep) ] -> TacNonTerm (!@loc,nt,po) ] ] - ; END |