diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/cLexer.ml | 78 | ||||
| -rw-r--r-- | parsing/cLexer.mli | 2 | ||||
| -rw-r--r-- | parsing/extend.ml | 2 | ||||
| -rw-r--r-- | parsing/g_constr.mlg | 85 | ||||
| -rw-r--r-- | parsing/g_prim.mlg | 15 | ||||
| -rw-r--r-- | parsing/notation_gram.ml | 2 | ||||
| -rw-r--r-- | parsing/notgram_ops.ml | 2 | ||||
| -rw-r--r-- | parsing/notgram_ops.mli | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 22 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 8 | ||||
| -rw-r--r-- | parsing/ppextend.ml | 2 | ||||
| -rw-r--r-- | parsing/ppextend.mli | 2 | ||||
| -rw-r--r-- | parsing/tok.ml | 2 | ||||
| -rw-r--r-- | parsing/tok.mli | 2 |
14 files changed, 143 insertions, 83 deletions
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index 42ca5f8c05..a27d6450b7 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -548,7 +548,7 @@ let peek_marker s = | ('a'..'z' | 'A'..'Z' | '_') -> ImmediateAsciiIdent | _ -> raise Stream.Failure -let parse_quotation loc s = +let parse_quotation loc bp s = match peek_marker s with | ImmediateAsciiIdent -> let c = Stream.next s in @@ -556,34 +556,42 @@ let parse_quotation loc s = try ident_tail loc (store 0 c) s with Stream.Failure -> raise (Stream.Error "") in - get_buff len + get_buff len, set_loc_pos loc bp (Stream.count s) | Delimited (lenmarker, bmarker, emarker) -> let b = Buffer.create 80 in let commit1 c = Buffer.add_char b c; Stream.junk s in let commit l = List.iter commit1 l in - let rec quotation depth = + let rec quotation loc depth = match Stream.npeek lenmarker s with | l when l = bmarker -> commit l; - quotation (depth + 1) + quotation loc (depth + 1) | l when l = emarker -> commit l; - if depth > 1 then quotation (depth - 1) + if depth > 1 then quotation loc (depth - 1) else loc + | '\n' :: cs -> + commit1 '\n'; + let loc = bump_loc_line_last loc (Stream.count s) in + quotation loc depth | c :: cs -> commit1 c; - quotation depth + quotation loc depth | [] -> raise Stream.Failure in - quotation 0; - Buffer.contents b + let loc = quotation loc 0 in + Buffer.contents b, set_loc_pos loc bp (Stream.count s) -let find_keyword loc id s = +let find_keyword loc id bp s = let tt = ttree_find !token_tree id in match progress_further loc tt.node 0 tt s with | None -> raise Not_found - | Some (c,NoQuotation) -> KEYWORD c - | Some (c,Quotation) -> QUOTATION(c, parse_quotation loc s) + | Some (c,NoQuotation) -> + let ep = Stream.count s in + KEYWORD c, set_loc_pos loc bp ep + | Some (c,Quotation) -> + let txt, loc = parse_quotation loc bp s in + QUOTATION(c, txt), loc let process_sequence loc bp c cs = let rec aux n cs = @@ -599,7 +607,9 @@ let process_chars ~diff_mode loc bp c cs = let ep = Stream.count cs in match t with | Some (t,NoQuotation) -> (KEYWORD t, set_loc_pos loc bp ep) - | Some (c,Quotation) -> (QUOTATION(c, parse_quotation loc cs), set_loc_pos loc bp ep) + | Some (c,Quotation) -> + let txt, loc = parse_quotation loc bp cs in + QUOTATION(c, txt), loc | None -> let ep' = bp + utf8_char_size loc cs c in if diff_mode then begin @@ -623,14 +633,21 @@ let parse_after_dot ~diff_mode loc c bp s = match Stream.peek s with Stream.Failure -> raise (Stream.Error "") in let field = get_buff len in - (try find_keyword loc ("."^field) s with Not_found -> FIELD field) + begin try find_keyword loc ("."^field) bp s + with Not_found -> + let ep = Stream.count s in + FIELD field, set_loc_pos loc bp ep end | _ -> match lookup_utf8 loc s with | Utf8Token (st, n) when Unicode.is_valid_ident_initial st -> let len = ident_tail loc (nstore n 0 s) s in let field = get_buff len in - (try find_keyword loc ("."^field) s with Not_found -> FIELD field) - | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars ~diff_mode loc bp c s) + begin try find_keyword loc ("."^field) bp s + with Not_found -> + let ep = Stream.count s in + FIELD field, set_loc_pos loc bp ep end + | AsciiChar | Utf8Token _ | EmptyStream -> + process_chars ~diff_mode loc bp c s (* Parse what follows a question mark *) @@ -664,22 +681,23 @@ let rec next_token ~diff_mode loc s = comm_loc bp; push_char c; next_token ~diff_mode loc s | Some ('.' as c) -> Stream.junk s; - let t = + let t, newloc = try parse_after_dot ~diff_mode loc c bp s with Stream.Failure -> raise (Stream.Error "") in - let ep = Stream.count s in comment_stop bp; (* We enforce that "." should either be part of a larger keyword, for instance ".(", or followed by a blank or eof. *) let () = match t with - | KEYWORD ("." | "...") -> - if not (blank_or_eof s) then - err (set_loc_pos loc bp (ep+1)) Undefined_token; - between_commands := true; - | _ -> () + | KEYWORD ("." | "...") -> + if not (blank_or_eof s) then begin + let ep = Stream.count s in + err (set_loc_pos loc bp (ep+1)) Undefined_token + end; + between_commands := true; + | _ -> () in - t, set_loc_pos loc bp ep + t, newloc | Some ('-' | '+' | '*' as c) -> Stream.junk s; let t,new_between_commands = @@ -698,10 +716,12 @@ let rec next_token ~diff_mode loc s = try ident_tail loc (store 0 c) s with Stream.Failure -> raise (Stream.Error "") in - let ep = Stream.count s in let id = get_buff len in comment_stop bp; - (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep + begin try find_keyword loc id bp s + with Not_found -> + let ep = Stream.count s in + IDENT id, set_loc_pos loc bp ep end | Some ('0'..'9') -> let n = NumTok.parse s in let ep = Stream.count s in @@ -745,9 +765,11 @@ let rec next_token ~diff_mode loc s = | Utf8Token (st, n) when Unicode.is_valid_ident_initial st -> let len = ident_tail loc (nstore n 0 s) s in let id = get_buff len in - let ep = Stream.count s in comment_stop bp; - (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep + begin try find_keyword loc id bp s + with Not_found -> + let ep = Stream.count s in + IDENT id, set_loc_pos loc bp ep end | AsciiChar | Utf8Token _ -> let t = process_chars ~diff_mode loc bp (Stream.next s) s in comment_stop bp; t diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 464bcf614d..964689f5f5 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/parsing/extend.ml b/parsing/extend.ml index dd7c301dfb..63e121c0d1 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 6df97609f5..8fdec7d1a8 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -31,8 +31,10 @@ let ldots_var = Id.of_string ".." let constr_kw = [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; "end"; "as"; "let"; "if"; "then"; "else"; "return"; - "SProp"; "Prop"; "Set"; "Type"; ".("; "_"; ".."; - "`{"; "`("; "{|"; "|}" ] + "SProp"; "Prop"; "Set"; "Type"; + ":="; "=>"; "->"; ".."; "<:"; "<<:"; ":>"; + ".("; "()"; "`{"; "`("; "@{"; "{|"; + "_"; "@"; "+"; "!"; "?"; ";"; ","; ":" ] let _ = List.iter CLexer.add_keyword constr_kw @@ -131,7 +133,8 @@ let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None } GRAMMAR EXTEND Gram - GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family + GLOBAL: binder_constr lconstr constr operconstr + universe_level universe_name sort sort_family global constr_pattern lconstr_pattern Constr.ident closed_binder open_binders binder binders binders_fixannot record_declaration typeclass_constraint pattern appl_arg; @@ -151,11 +154,12 @@ GRAMMAR EXTEND Gram [ [ c = lconstr -> { c } ] ] ; sort: - [ [ "Set" -> { GSet } - | "Prop" -> { GProp } - | "SProp" -> { GSProp } - | "Type" -> { GType [] } - | "Type"; "@{"; u = universe; "}" -> { GType u } + [ [ "Set" -> { UNamed [GSet,0] } + | "Prop" -> { UNamed [GProp,0] } + | "SProp" -> { UNamed [GSProp,0] } + | "Type" -> { UAnonymous {rigid=true} } + | "Type"; "@{"; "_"; "}" -> { UAnonymous {rigid=false} } + | "Type"; "@{"; u = universe; "}" -> { UNamed u } ] ] ; sort_family: @@ -165,11 +169,17 @@ GRAMMAR EXTEND Gram | "Type" -> { Sorts.InType } ] ] ; + universe_increment: + [ [ "+"; n = natural -> { n } + | -> { 0 } ] ] + ; + universe_name: + [ [ id = global -> { GType id } + | "Set" -> { GSet } + | "Prop" -> { GProp } ] ] + ; universe_expr: - [ [ id = global; "+"; n = natural -> { Some (id,n) } - | id = global -> { Some (id,0) } - | "_" -> { None } - ] ] + [ [ id = universe_name; n = universe_increment -> { (id,n) } ] ] ; universe: [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { ids } @@ -225,11 +235,13 @@ GRAMMAR EXTEND Gram [ c=atomic_constr -> { c } | c=match_constr -> { c } | "("; c = operconstr LEVEL "200"; ")" -> - { (match c.CAst.v with + { (* Preserve parentheses around numerals so that constrintern does not + collapse -(3) into the numeral -3. *) + (match c.CAst.v with | CPrim (Numeral (SPlus,n)) -> CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[])) | _ -> c) } - | "{|"; c = record_declaration; "|}" -> { c } + | "{|"; c = record_declaration; bar_cbrace -> { c } | "{"; c = binder_constr ; "}" -> { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) } | "`{"; c = operconstr LEVEL "200"; "}" -> @@ -277,16 +289,16 @@ GRAMMAR EXTEND Gram ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) } - | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; + | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCases (LetPatternStyle, None, [c1, None, None], [CAst.make ~loc ([[p]], c2)]) } - | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; + | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc ([[p]], c2)]) } - | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200"; + | "let"; "'"; p = pattern LEVEL "200"; "in"; t = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ @@ -324,12 +336,12 @@ GRAMMAR EXTEND Gram | -> { None } ] ] ; universe_level: - [ [ "Set" -> { GSet } + [ [ "Set" -> { UNamed GSet } (* no parsing SProp as a level *) - | "Prop" -> { GProp } - | "Type" -> { GType UUnknown } - | "_" -> { GType UAnonymous } - | id = global -> { GType (UNamed id) } + | "Prop" -> { UNamed GProp } + | "Type" -> { UAnonymous {rigid=true} } + | "_" -> { UAnonymous {rigid=false} } + | id = global -> { UNamed (GType id) } ] ] ; fix_constr: @@ -359,7 +371,7 @@ GRAMMAR EXTEND Gram case_item: [ [ c=operconstr LEVEL "100"; ona = OPT ["as"; id=name -> { id } ]; - ty = OPT ["in"; t=pattern -> { t } ] -> + ty = OPT ["in"; t = pattern LEVEL "200" -> { t } ] -> { (c,ona,ty) } ] ] ; case_type: @@ -377,14 +389,14 @@ GRAMMAR EXTEND Gram [ [ OPT"|"; br=LIST0 eqn SEP "|" -> { br } ] ] ; mult_pattern: - [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> { pl } ] ] + [ [ pl = LIST1 pattern LEVEL "200" SEP "," -> { pl } ] ] ; eqn: [ [ pll = LIST1 mult_pattern SEP "|"; "=>"; rhs = lconstr -> { (CAst.make ~loc (pll,rhs)) } ] ] ; record_pattern: - [ [ id = global; ":="; pat = pattern -> { (id, pat) } ] ] + [ [ id = global; ":="; pat = pattern LEVEL "200" -> { (id, pat) } ] ] ; record_patterns: [ [ p = record_pattern; ";"; ps = record_patterns -> { p :: ps } @@ -396,7 +408,10 @@ GRAMMAR EXTEND Gram pattern: [ "200" RIGHTA [ ] | "100" RIGHTA - [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> { CAst.make ~loc @@ CPatOr (p::pl) } ] + [ p = pattern; ":"; ty = binder_constr -> + {CAst.make ~loc @@ CPatCast (p, ty) } + | p = pattern; ":"; ty = operconstr LEVEL "100" -> + {CAst.make ~loc @@ CPatCast (p, ty) } ] | "99" RIGHTA [ ] | "90" RIGHTA [ ] | "10" LEFTA @@ -409,21 +424,17 @@ GRAMMAR EXTEND Gram [ c = pattern; "%"; key=IDENT -> { CAst.make ~loc @@ CPatDelimiters (key,c) } ] | "0" [ r = Prim.reference -> { CAst.make ~loc @@ CPatAtom (Some r) } - | "{|"; pat = record_patterns; "|}" -> { CAst.make ~loc @@ CPatRecord pat } + | "{|"; pat = record_patterns; bar_cbrace -> { CAst.make ~loc @@ CPatRecord pat } | "_" -> { CAst.make ~loc @@ CPatAtom None } | "("; p = pattern LEVEL "200"; ")" -> - { (match p.CAst.v with + { (* Preserve parentheses around numerals so that constrintern does not + collapse -(3) into the numeral -3. *) + (match p.CAst.v with | CPatPrim (Numeral (SPlus,n)) -> CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) | _ -> p) } - | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" -> - { let p = - match p with - | { CAst.v = CPatPrim (Numeral (SPlus,n)) } -> - CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) - | _ -> p - in - CAst.make ~loc @@ CPatCast (p, ty) } + | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" -> + { CAst.make ~loc @@ CPatOr (p::pl) } | n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (SPlus,n)) } | s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ] ; diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 80dd997860..c1f52c5b39 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -15,7 +15,7 @@ open Libnames open Pcoq.Prim -let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"] +let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"; "%"; "|"] let _ = List.iter CLexer.add_keyword prim_kw @@ -31,13 +31,19 @@ let my_int_of_string loc s = with Failure _ -> CErrors.user_err ~loc (Pp.str "This number is too large.") +let check_nospace loc expected = + let (bp, ep) = Loc.unloc loc in + if ep = bp + String.length expected then () else + Gramlib.Ploc.raise loc (Stream.Error ("'" ^ expected ^ "' expected")) + } GRAMMAR EXTEND Gram GLOBAL: bigint natural integer identref name ident var preident fullyqualid qualid reference dirpath ne_lstring - ne_string string lstring pattern_ident pattern_identref by_notation smart_global; + ne_string string lstring pattern_ident pattern_identref by_notation + smart_global bar_cbrace; preident: [ [ s = IDENT -> { s } ] ] ; @@ -123,4 +129,7 @@ GRAMMAR EXTEND Gram bigint: (* Negative numbers are dealt with elsewhere *) [ [ i = NUMERAL -> { check_int loc i } ] ] ; + bar_cbrace: + [ [ "|"; "}" -> { check_nospace loc "|}" } ] ] + ; END diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml index 6df0d6f21a..9f133ca9d4 100644 --- a/parsing/notation_gram.ml +++ b/parsing/notation_gram.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml index 5cc1292c92..009dafdb13 100644 --- a/parsing/notgram_ops.ml +++ b/parsing/notgram_ops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli index f427a607b7..c31f4505e7 100644 --- a/parsing/notgram_ops.mli +++ b/parsing/notgram_ops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 8f38e437b4..3aaba27579 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -363,8 +363,21 @@ end module Grammar = Register(GrammarObj) +let warn_deprecated_intropattern = + let open CWarnings in + create ~name:"deprecated-intropattern-entry" ~category:"deprecated" + (fun () -> Pp.strbrk "Entry name intropattern has been renamed in order \ + to be consistent with the documented grammar of tactics. Use \ + \"simple_intropattern\" instead.") + +let check_compatibility = function + | Genarg.ExtraArg s when ArgT.repr s = "intropattern" -> warn_deprecated_intropattern () + | _ -> () + let register_grammar = Grammar.register0 -let genarg_grammar = Grammar.obj +let genarg_grammar x = + check_compatibility x; + Grammar.obj x let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Entry.t = let e = new_entry u s in @@ -411,6 +424,8 @@ module Prim = let ne_string = Entry.create "Prim.ne_string" let ne_lstring = Entry.create "Prim.ne_lstring" + let bar_cbrace = Entry.create "'|}'" + end module Constr = @@ -425,6 +440,7 @@ module Constr = let binder_constr = gec_constr "binder_constr" let ident = make_gen_entry uconstr "ident" let global = make_gen_entry uconstr "global" + let universe_name = make_gen_entry uconstr "universe_name" let universe_level = make_gen_entry uconstr "universe_level" let sort = make_gen_entry uconstr "sort" let sort_family = make_gen_entry uconstr "sort_family" @@ -585,7 +601,7 @@ let unfreeze (grams, lex) = (** No need to provide an init function : the grammar state is statically available, and already empty initially, while - the lexer state should not be resetted, since it contains + the lexer state should not be reset, since it contains keywords declared in g_*.ml4 *) let parser_summary_tag = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 3a57c14a3b..cde867d2ef 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -38,9 +38,9 @@ end - dynamic rules declared at the evaluation of Coq files (using e.g. Notation, Infix, or Tactic Notation) - - static rules explicitly defined in files g_*.ml4 + - static rules explicitly defined in files g_*.mlg - static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and - VERNAC EXTEND (see e.g. file extratactics.ml4) + VERNAC EXTEND (see e.g. file extratactics.mlg) Note that parsing a Coq document is in essence stateful: the parser needs to recognize commands that start proofs and use a different @@ -170,6 +170,7 @@ module Prim : val ne_string : string Entry.t val ne_lstring : lstring Entry.t val var : lident Entry.t + val bar_cbrace : unit Entry.t end module Constr : @@ -181,6 +182,7 @@ module Constr : val operconstr : constr_expr Entry.t val ident : Id.t Entry.t val global : qualid Entry.t + val universe_name : Glob_term.glob_sort_name Entry.t val universe_level : Glob_term.glob_level Entry.t val sort : Glob_term.glob_sort Entry.t val sort_family : Sorts.family Entry.t diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml index e1f5e20117..7368f4109e 100644 --- a/parsing/ppextend.ml +++ b/parsing/ppextend.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli index 7eb5967a3e..be5af75e72 100644 --- a/parsing/ppextend.mli +++ b/parsing/ppextend.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/parsing/tok.ml b/parsing/tok.ml index 71e2d4aa80..419b5a3d7f 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/parsing/tok.mli b/parsing/tok.mli index a5fb5ad9cd..a6cb4f8506 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) |