summaryrefslogtreecommitdiff
path: root/parsing/g_basevernac.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_basevernac.ml4')
-rw-r--r--parsing/g_basevernac.ml4524
1 files changed, 0 insertions, 524 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
deleted file mode 100644
index c4badbc3..00000000
--- a/parsing/g_basevernac.ml4
+++ /dev/null
@@ -1,524 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* $Id: g_basevernac.ml4,v 1.83.2.2 2004/07/16 19:30:37 herbelin Exp $ *)
-
-open Coqast
-open Extend
-open Ppextend
-open Vernacexpr
-open Pcoq
-open Vernac_
-open Goptions
-open Constr
-open Prim
-
-let vernac_kw =
- [ "Quit"; "Load"; "Compile"; "Fixpoint"; "CoFixpoint";
- "Definition"; "Inductive"; "CoInductive";
- "Theorem"; "Variable"; "Axiom"; "Parameter"; "Hypothesis";
- "."; ">->" ]
-let _ =
- if !Options.v7 then
- List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
-
-let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
-let lstring = Gram.Entry.create "lstring"
-
-
-if !Options.v7 then
-GEXTEND Gram
- GLOBAL: class_rawexpr;
-
- class_rawexpr:
- [ [ IDENT "FUNCLASS" -> FunClass
- | IDENT "SORTCLASS" -> SortClass
- | qid = global -> RefClass qid ] ]
- ;
-END;
-
-if !Options.v7 then
-GEXTEND Gram
- GLOBAL: command lstring;
-
- lstring:
- [ [ s = STRING -> s ] ]
- ;
- comment:
- [ [ c = constr -> CommentConstr c
- | s = STRING -> CommentString s
- | n = natural -> CommentInt n ] ]
- ;
- command:
- [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l
-
- (* System directory *)
- | IDENT "Pwd" -> VernacChdir None
- | IDENT "Cd" -> VernacChdir None
- | IDENT "Cd"; dir = lstring -> VernacChdir (Some dir)
-
- (* Toplevel control *)
- | IDENT "Drop" -> VernacToplevelControl Drop
- | IDENT "ProtectedLoop" -> VernacToplevelControl ProtectedLoop
- | "Quit" -> VernacToplevelControl Quit
-
- (* Dump of the universe graph - to file or to stdout *)
- | IDENT "Dump"; IDENT "Universes"; fopt = OPT lstring ->
- VernacPrint (PrintUniverses fopt)
-
- | IDENT "Locate"; l = locatable -> VernacLocate l
-
- (* Managing load paths *)
- | IDENT "Add"; IDENT "LoadPath"; dir = lstring; alias = as_dirpath ->
- VernacAddLoadPath (false, dir, alias)
- | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = lstring;
- alias = as_dirpath -> VernacAddLoadPath (true, dir, alias)
- | IDENT "Remove"; IDENT "LoadPath"; dir = lstring ->
- VernacRemoveLoadPath dir
-
- (* For compatibility *)
- | IDENT "AddPath"; dir = lstring; alias = as_dirpath ->
- VernacAddLoadPath (false, dir, alias)
- | IDENT "AddRecPath"; dir = lstring; alias = as_dirpath ->
- VernacAddLoadPath (true, dir, alias)
- | IDENT "DelPath"; dir = lstring ->
- VernacRemoveLoadPath dir
-
- (* Printing (careful factorization of entries) *)
- | IDENT "Print"; p = printable -> VernacPrint p
- | IDENT "Print"; qid = global -> VernacPrint (PrintName qid)
- | IDENT "Print" -> VernacPrint PrintLocalContext
- | IDENT "Print"; IDENT "Module"; "Type"; qid = global ->
- VernacPrint (PrintModuleType qid)
- | IDENT "Print"; IDENT "Module"; qid = global ->
- VernacPrint (PrintModule qid)
- | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n)
- | IDENT "About"; qid = global -> VernacPrint (PrintAbout qid)
-
- (* Searching the environment *)
- | IDENT "Search"; qid = global; l = in_or_out_modules ->
- VernacSearch (SearchHead qid, 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";
- sl = [ "["; l = LIST1 [ r = global -> SearchRef r
- | s = lstring -> SearchString s ]; "]" -> l
- | qid = global -> [SearchRef qid] ];
- l = in_or_out_modules ->
- VernacSearch (SearchAbout sl, l)
-
- (* TODO: rapprocher Eval et Check *)
- | IDENT "Eval"; r = Tactic.red_expr; "in";
- c = constr -> VernacCheckMayEval (Some r, None, c)
- | IDENT "Check"; c = constr ->
- VernacCheckMayEval (None, None, c)
- | "Type"; c = constr -> VernacGlobalCheck c (* pas dans le RefMan *)
-
- | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = lstring ->
- VernacAddMLPath (false, dir)
- | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = lstring ->
- VernacAddMLPath (true, dir)
-(*
- | IDENT "SearchIsos"; c = constr -> VernacSearch (SearchIsos c)
-*)
-
- (* Pour intervenir sur les tables de paramètres *)
-
- | "Set"; table = IDENT; field = IDENT; v = option_value ->
- VernacSetOption (SecondaryTable (table,field),v)
- | "Set"; table = IDENT; field = IDENT; lv = LIST1 option_ref_value ->
- VernacAddOption (SecondaryTable (table,field),lv)
- | "Set"; table = IDENT; field = IDENT ->
- VernacSetOption (SecondaryTable (table,field),BoolValue true)
- | IDENT "Unset"; table = IDENT; field = IDENT ->
- VernacUnsetOption (SecondaryTable (table,field))
- | IDENT "Unset"; table = IDENT; field = IDENT; lv = LIST1 option_ref_value ->
- VernacRemoveOption (SecondaryTable (table,field),lv)
- | "Set"; table = IDENT; value = option_value ->
- VernacSetOption (PrimaryTable table, value)
- | "Set"; table = IDENT ->
- VernacSetOption (PrimaryTable table, BoolValue true)
- | IDENT "Unset"; table = IDENT ->
- VernacUnsetOption (PrimaryTable table)
-
- | IDENT "Print"; IDENT "Table"; table = IDENT; field = IDENT ->
- VernacPrintOption (SecondaryTable (table,field))
- | IDENT "Print"; IDENT "Table"; table = IDENT ->
- VernacPrintOption (PrimaryTable table)
-
- | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value
- -> VernacAddOption (SecondaryTable (table,field), v)
-
- (* Un value global ci-dessous va être caché par un field au dessus! *)
- | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value ->
- VernacAddOption (PrimaryTable table, v)
-
- | IDENT "Test"; table = IDENT; field = IDENT; v = LIST1 option_ref_value
- -> VernacMemOption (SecondaryTable (table,field), v)
- | IDENT "Test"; table = IDENT; field = IDENT ->
- VernacPrintOption (SecondaryTable (table,field))
- | IDENT "Test"; table = IDENT; v = LIST1 option_ref_value ->
- VernacMemOption (PrimaryTable table, v)
- | IDENT "Test"; table = IDENT ->
- VernacPrintOption (PrimaryTable table)
-
- | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value
- -> VernacRemoveOption (SecondaryTable (table,field), v)
- | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value ->
- VernacRemoveOption (PrimaryTable table, v) ] ]
- ;
- printable:
- [ [ IDENT "Term"; qid = global -> PrintOpaqueName qid
- | IDENT "All" -> PrintFullContext
- | IDENT "Section"; s = global -> PrintSectionContext s
- | IDENT "Grammar"; uni = IDENT; ent = IDENT ->
- (* This should be in "syntax" section but is here for factorization*)
- PrintGrammar (uni, ent)
- | IDENT "LoadPath" -> PrintLoadPath
- | IDENT "Modules" -> PrintModules
-
- | IDENT "ML"; IDENT "Path" -> PrintMLLoadPath
- | IDENT "ML"; IDENT "Modules" -> PrintMLModules
- | IDENT "Graph" -> PrintGraph
- | IDENT "Classes" -> PrintClasses
- | IDENT "Coercions" -> PrintCoercions
- | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
- -> PrintCoercionPaths (s,t)
- | IDENT "Tables" -> PrintTables
- | "Proof"; qid = global -> PrintOpaqueName qid
- | IDENT "Hint" -> PrintHintGoal
- | IDENT "Hint"; qid = global -> PrintHint qid
- | IDENT "Hint"; "*" -> PrintHintDb
- | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
- | IDENT "Scopes" -> PrintScopes
- | IDENT "Scope"; s = IDENT -> PrintScope s
- | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
- | IDENT "Implicit"; qid = global -> PrintImplicit qid ] ]
- ;
- locatable:
- [ [ qid = global -> LocateTerm qid
- | IDENT "File"; f = lstring -> LocateFile f
- | IDENT "Library"; qid = global -> LocateLibrary qid
- | s = lstring -> LocateNotation s ] ]
- ;
- option_value:
- [ [ n = integer -> IntValue n
- | s = lstring -> StringValue s ] ]
- ;
- option_ref_value:
- [ [ id = global -> QualidRefValue id
- | s = lstring -> StringRefValue s ] ]
- ;
- as_dirpath:
- [ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ]
- ;
- in_or_out_modules:
- [ [ IDENT "inside"; l = LIST1 global -> SearchInside l
- | IDENT "outside"; l = LIST1 global -> SearchOutside l
- | -> SearchOutside [] ] ]
- ;
-END
-
-(* Grammar extensions *)
-
-(* automatic translation of levels *)
-let adapt_level n =
- if n >= 10 then n*10 else
- [| 0; 20; 30; 40; 50; 70; 80; 85; 90; 95; 100|].(n)
-
-let map_modl = function
- | SetItemLevel(ids,NumLevel n) -> SetItemLevel(ids,NumLevel (adapt_level n))
- | SetLevel n -> SetLevel(adapt_level n)
- | m -> m
-
-if !Options.v7 then
-GEXTEND Gram
- GLOBAL: syntax;
-
- univ:
- [ [ univ = IDENT ->
- set_default_action_parser (parser_type_from_name univ); univ ] ]
- ;
- syntax:
- [ [ IDENT "Token"; s = lstring ->
- Pp.warning "Token declarations are now useless"; VernacNop
-
- | IDENT "Grammar"; IDENT "tactic"; IDENT "simple_tactic";
- OPT [ ":"; IDENT "tactic" ]; ":=";
- OPT "|"; tl = LIST0 grammar_tactic_rule SEP "|" ->
- VernacTacticGrammar tl
-
- | IDENT "Grammar"; u = univ;
- tl = LIST1 grammar_entry SEP "with" ->
- VernacGrammar (rename_command_entry u,tl)
-
- | IDENT "Syntax"; u = univ; el = LIST1 syntax_entry SEP ";" ->
- VernacSyntax (u,el)
-
- | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = lstring;
- modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
- (s8,mv8) =
- [IDENT "V8only";
- s8=OPT lstring;
- mv8=OPT["(";mv8=LIST1 syntax_modifier SEP ","; ")" -> mv8] ->
- (s8,mv8)
- | -> (None,None)] ->
- let s8 = match s8 with Some s -> s | _ -> s in
- let mv8 = match mv8 with
- Some mv8 -> mv8
- | _ -> List.map map_modl modl in
- VernacSyntaxExtension (local,Some (s,modl),Some(s8,mv8))
-
- | IDENT "Uninterpreted"; IDENT "V8Notation"; local = locality; s = lstring;
- modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
- VernacSyntaxExtension (local,None,Some(s,modl))
-
- | IDENT "Open"; local = locality; IDENT "Scope";
- sc = IDENT -> VernacOpenCloseScope (local,true, sc)
-
- | IDENT "Close"; local = locality; IDENT "Scope";
- sc = IDENT -> VernacOpenCloseScope (local,false,sc)
-
- | IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
- VernacDelimiters (sc,key)
-
- | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
- refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
-
- | IDENT "Arguments"; IDENT "Scope"; qid = global;
- "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
-
- | IDENT "Infix"; local = locality; a = entry_prec; n = OPT natural;
- op = lstring;
- p = global;
- modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
- sc = OPT [ ":"; sc = IDENT -> sc];
- mv8 =
- [IDENT "V8only";
- a8=entry_prec;
- n8=OPT natural;
- op8=OPT lstring;
- mv8=["("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> []]
- ->
- (match (a8,n8,mv8,op8) with
- | None,None,[],None -> None
- | _,_,mv8,_ ->
- Some(op8,Metasyntax.merge_modifiers a8 n8 mv8))
- | -> (* Means: rules are based on V7 rules *)
- Some (None,[]) ] ->
- let mv = Metasyntax.merge_modifiers a n modl in
- let v8 = Util.option_app (function (op8,mv8) ->
- let op8 = match op8 with None -> op | Some op -> op in
- let mv8 =
- if mv8=[] then
- let mv8 = List.map map_modl mv in
- let mv8 = if List.for_all
- (function SetLevel _ -> false | _ -> true) mv8
- then SetLevel 10 :: mv8 else mv8 in
- let mv8 = if List.for_all
- (function SetAssoc _ -> false | _ -> true) mv8
- then SetAssoc Gramext.LeftA :: mv8 else mv8 in
- mv8
- else mv8 in
- (op8,mv8)) mv8 in
- VernacInfix (local,(op,mv),p,v8,sc)
- | IDENT "Distfix"; local = locality; a = entry_prec; n = natural;
- s = lstring; p = global; sc = OPT [ ":"; sc = IDENT -> sc ] ->
- let (a,s,c) = Metasyntax.translate_distfix a s p in
- let mv = Some(s,[SetLevel n;SetAssoc a]) in
- VernacNotation (local,c,mv,mv,sc)
-(*
- VernacDistfix (local,a,n,s,p,sc)
-*)
- | IDENT "Notation"; local = locality; id = ident; ":="; c = constr;
- b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] ->
- VernacSyntacticDefinition (id,c,local,b)
- | IDENT "Notation"; local = locality; s = lstring; ":="; c = constr;
- modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
- sc = OPT [ ":"; sc = IDENT -> sc ];
- (s8,mv8) =
- [IDENT "V8only";
- s8=OPT lstring;
- mv8=OPT["(";mv8=LIST1 syntax_modifier SEP ","; ")" -> mv8] ->
- (s8,mv8)
- | -> (* Means: rules are based on V7 rules *)
- None, Some [] ] ->
- let smv8 = match s8,mv8 with
- | None, None -> None (* = only interpretation *)
- | Some s8, None -> Some (s8,[]) (* = only interp, new s *)
- | None, Some [] -> Some (s,List.map map_modl modl) (*like v7*)
- | None, Some mv8 -> Some (s,mv8) (* s like v7 *)
- | Some s8, Some mv8 -> Some (s8,mv8) in
- VernacNotation (local,c,Some(s,modl),smv8,sc)
- | IDENT "V8Notation"; local = locality; s = lstring; ":="; c = constr;
- modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
- sc = OPT [ ":"; sc = IDENT -> sc ] ->
- VernacNotation (local,c,None,Some(s,modl),sc)
-
- | IDENT "V8Infix"; local = locality; op8 = lstring; p = global;
- modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
- sc = OPT [ ":"; sc = IDENT -> sc] ->
- let mv8 = Metasyntax.merge_modifiers None None modl in
- VernacInfix (local,("",[]),p,Some (op8,mv8),sc)
-
- (* "Print" "Grammar" should be here but is in "command" entry in order
- to factorize with other "Print"-based vernac entries *)
- ] ]
- ;
- locality:
- [ [ IDENT "Local" -> true | -> false ] ]
- ;
- level:
- [ [ IDENT "level"; n = natural -> NumLevel n
- | IDENT "next"; IDENT "level" -> NextLevel ] ]
- ;
- syntax_modifier:
- [ [ x = IDENT; IDENT "at"; lev = level -> SetItemLevel ([x],lev)
- | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; lev = level ->
- SetItemLevel (x::l,lev)
- | IDENT "at"; IDENT "level"; n = natural -> SetLevel n
- | IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA
- | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA
- | IDENT "no"; IDENT "associativity" -> SetAssoc Gramext.NonA
- | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
- | IDENT "only"; IDENT "parsing" -> SetOnlyParsing
- | IDENT "format"; s = [s = lstring -> (loc,s)] -> SetFormat s ] ]
- ;
- syntax_extension_type:
- [ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference
- | IDENT "bigint" -> ETBigint
- | i=IDENT -> ETOther ("constr",i)
- ] ]
- ;
- opt_scope:
- [ [ IDENT "_" -> None | sc = IDENT -> Some sc ] ]
- ;
- (* Syntax entries for Grammar. Only grammar_entry is exported *)
- grammar_entry:
- [[ nont = IDENT; set_entry_type; ":=";
- ep = entry_prec; OPT "|"; rl = LIST0 grammar_rule SEP "|" ->
- (rename_command_entry nont,ep,rl) ]]
- ;
- entry_prec:
- [[ IDENT "LEFTA" -> Some Gramext.LeftA
- | IDENT "RIGHTA" -> Some Gramext.RightA
- | IDENT "NONA" -> Some Gramext.NonA
- | -> None ]]
- ;
- grammar_tactic_rule:
- [[ name = rule_name; "["; s = lstring; pil = LIST0 production_item; "]";
- "->"; "["; t = Tactic.tactic; "]" -> (name, (s,pil), t) ]]
- ;
- grammar_rule:
- [[ name = rule_name; "["; pil = LIST0 production_item; "]"; "->";
- a = action -> (name, pil, a) ]]
- ;
- rule_name:
- [[ name = IDENT -> name ]]
- ;
- production_item:
- [[ s = lstring -> VTerm s
- | nt = non_terminal; po = OPT [ "("; p = METAIDENT; ")" -> p ] ->
- match po with
- | Some p -> VNonTerm (loc,nt,Some (Names.id_of_string p))
- | _ -> VNonTerm (loc,nt,None) ]]
- ;
- non_terminal:
- [[ u = IDENT; ":"; nt = IDENT ->
- NtQual(rename_command_entry u, rename_command_entry nt)
- | nt = IDENT -> NtShort (rename_command_entry nt) ]]
- ;
-
-
- (* Syntax entries for Syntax. Only syntax_entry is exported *)
- syntax_entry:
- [ [ IDENT "level"; p = precedence; ":";
- OPT "|"; rl = LIST1 syntax_rule SEP "|" -> (p,rl) ] ]
- ;
- syntax_rule:
- [ [ nm = IDENT; "["; s = astpat; "]"; "->"; u = unparsing -> (nm,s,u) ] ]
- ;
- precedence:
- [ [ a = natural -> a
-(* | "["; a1 = natural; a2 = natural; a3 = natural; "]" -> (a1,a2,a3)*)
- ] ]
- ;
- unparsing:
- [ [ "["; ll = LIST0 next_hunks; "]" -> ll ] ]
- ;
- next_hunks:
- [ [ IDENT "FNL" -> UNP_FNL
- | IDENT "TAB" -> UNP_TAB
- | c = lstring -> RO c
- | "[";
- x =
- [ b = box; ll = LIST0 next_hunks -> UNP_BOX (b,ll)
- | n = natural; m = natural -> UNP_BRK (n, m)
- | IDENT "TBRK"; n = natural; m = natural -> UNP_TBRK (n, m) ];
- "]" -> x
- | e = Prim.ast; oprec = OPT [ ":"; pr = paren_reln_or_extern -> pr ] ->
- match oprec with
- | Some (ext,pr) -> PH (e,ext,pr)
- | None -> PH (e,None,Any)
- ]]
- ;
- box:
- [ [ "<"; bk = box_kind; ">" -> bk ] ]
- ;
- box_kind:
- [ [ IDENT "h"; n = natural -> PpHB n
- | IDENT "v"; n = natural -> PpVB n
- | IDENT "hv"; n = natural -> PpHVB n
- | IDENT "hov"; n = natural -> PpHOVB n
- | IDENT "t" -> PpTB ] ]
- ;
- paren_reln_or_extern:
- [ [ IDENT "L" -> None, L
- | IDENT "E" -> None, E
- | pprim = lstring; precrec = OPT [ ":"; p = precedence -> p ] ->
- match precrec with
- | Some p -> Some pprim, Prec p
- | None -> Some pprim, Any ] ]
- ;
- (* meta-syntax entries *)
- astpat:
- [ [ "<<" ; a = Prim.ast; ">>" -> a
- | a = Constr.constr ->
- Termast.ast_of_rawconstr
- (Constrintern.interp_rawconstr Evd.empty (Global.env()) a)
- ] ]
- ;
- action:
- [ [ IDENT "let"; p = Prim.astlist; et = set_internal_entry_type;
- "="; e1 = action; "in"; e = action -> Ast.CaseAction (loc,e1,et,[p,e])
- | IDENT "case"; a = action; et = set_internal_entry_type; "of";
- cl = LIST1 case SEP "|"; IDENT "esac" -> Ast.CaseAction (loc,a,et,cl)
- | "["; a = default_action_parser; "]" -> Ast.SimpleAction (loc,a) ] ]
- ;
- case:
- [[ p = Prim.astlist; "->"; a = action -> (p,a) ]]
- ;
- set_internal_entry_type:
- [[ ":"; IDENT "ast"; IDENT "list" -> Ast.ETastl
- | [ ":"; IDENT "ast" -> () | -> () ] -> Ast.ETast ]]
- ;
- set_entry_type:
- [[ ":"; et = entry_type -> set_default_action_parser et
- | -> () ]]
- ;
- entry_type:
- [[ IDENT "ast"; IDENT "list" -> Util.error "type ast list no longer supported"
- | IDENT "ast" -> Util.error "type ast no longer supported"
- | IDENT "constr" -> ConstrParser
- | IDENT "pattern" -> CasesPatternParser
- | IDENT "tactic" -> assert false
- | IDENT "vernac" -> Util.error "vernac extensions no longer supported" ] ]
- ;
-END
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 04:37:36 +0000