aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--coqpp/coqpp_main.ml36
-rw-r--r--gramlib/grammar.ml2
-rw-r--r--gramlib/grammar.mli1
-rw-r--r--ide/idetop.ml6
-rw-r--r--parsing/pcoq.ml75
-rw-r--r--parsing/pcoq.mli17
-rw-r--r--plugins/ltac/g_tactic.mlg2
-rw-r--r--plugins/ltac/tacentries.ml36
-rw-r--r--plugins/ssr/ssrparser.mlg22
-rw-r--r--plugins/ssrmatching/g_ssrmatching.mlg2
-rw-r--r--stm/stm.mli4
-rw-r--r--toplevel/coqloop.ml10
-rw-r--r--toplevel/coqloop.mli2
-rw-r--r--toplevel/vernac.ml4
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg10
-rw-r--r--user-contrib/Ltac2/tac2core.ml42
-rw-r--r--user-contrib/Ltac2/tac2entries.ml16
-rw-r--r--user-contrib/Ltac2/tac2entries.mli2
-rw-r--r--vernac/egramcoq.ml72
-rw-r--r--vernac/egramml.ml16
-rw-r--r--vernac/egramml.mli4
-rw-r--r--vernac/metasyntax.ml4
-rw-r--r--vernac/proof_using.ml2
-rw-r--r--vernac/pvernac.ml10
-rw-r--r--vernac/vernacextend.ml22
-rw-r--r--vernac/vernacextend.mli2
-rw-r--r--vernac/vernacinterp.ml4
-rw-r--r--vernac/vernacstate.ml2
-rw-r--r--vernac/vernacstate.mli2
29 files changed, 210 insertions, 219 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 0e0aefaaef..43cd6f1784 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -115,7 +115,7 @@ let print_local fmt ext =
match locals with
| [] -> ()
| e :: locals ->
- let mk_e fmt e = fprintf fmt "Pcoq.Entry.create \"%s\"" e in
+ let mk_e fmt e = fprintf fmt "Pcoq.Entry.make \"%s\"" e in
let () = fprintf fmt "@[<hv 2>let %s =@ @[%a@]@]@ " e mk_e e in
let iter e = fprintf fmt "@[<hv 2>and %s =@ @[%a@]@]@ " e mk_e e in
let () = List.iter iter locals in
@@ -217,43 +217,43 @@ let rec print_prod fmt p =
and print_extrule fmt (tkn, vars, body) =
let tkn = List.rev tkn in
- fprintf fmt "@[Pcoq.G.Production.make@ @[(%a)@]@ @[(%a)@]@]" (print_symbols ~norec:false) tkn print_fun (vars, body)
+ fprintf fmt "@[Pcoq.Production.make@ @[(%a)@]@ @[(%a)@]@]" (print_symbols ~norec:false) tkn print_fun (vars, body)
and print_symbols ~norec fmt = function
-| [] -> fprintf fmt "Pcoq.G.Rule.stop"
+| [] -> fprintf fmt "Pcoq.Rule.stop"
| tkn :: tkns ->
- let c = if norec then "Pcoq.G.Rule.next_norec" else "Pcoq.G.Rule.next" in
+ let c = if norec then "Pcoq.Rule.next_norec" else "Pcoq.Rule.next" in
fprintf fmt "%s @[(%a)@ (%a)@]" c (print_symbols ~norec) tkns print_symbol tkn
and print_symbol fmt tkn = match tkn with
| SymbToken (t, s) ->
- fprintf fmt "(Pcoq.G.Symbol.token (%a))" print_tok (t, s)
+ fprintf fmt "(Pcoq.Symbol.token (%a))" print_tok (t, s)
| SymbEntry (e, None) ->
- fprintf fmt "(Pcoq.G.Symbol.nterm %s)" e
+ fprintf fmt "(Pcoq.Symbol.nterm %s)" e
| SymbEntry (e, Some l) ->
- fprintf fmt "(Pcoq.G.Symbol.nterml %s (%a))" e print_string l
+ fprintf fmt "(Pcoq.Symbol.nterml %s (%a))" e print_string l
| SymbSelf ->
- fprintf fmt "Pcoq.G.Symbol.self"
+ fprintf fmt "Pcoq.Symbol.self"
| SymbNext ->
- fprintf fmt "Pcoq.G.Symbol.next"
+ fprintf fmt "Pcoq.Symbol.next"
| SymbList0 (s, None) ->
- fprintf fmt "(Pcoq.G.Symbol.list0 %a)" print_symbol s
+ fprintf fmt "(Pcoq.Symbol.list0 %a)" print_symbol s
| SymbList0 (s, Some sep) ->
- fprintf fmt "(Pcoq.G.Symbol.list0sep (%a) (%a) false)" print_symbol s print_symbol sep
+ fprintf fmt "(Pcoq.Symbol.list0sep (%a) (%a) false)" print_symbol s print_symbol sep
| SymbList1 (s, None) ->
- fprintf fmt "(Pcoq.G.Symbol.list1 (%a))" print_symbol s
+ fprintf fmt "(Pcoq.Symbol.list1 (%a))" print_symbol s
| SymbList1 (s, Some sep) ->
- fprintf fmt "(Pcoq.G.Symbol.list1sep (%a) (%a) false)" print_symbol s print_symbol sep
+ fprintf fmt "(Pcoq.Symbol.list1sep (%a) (%a) false)" print_symbol s print_symbol sep
| SymbOpt s ->
- fprintf fmt "(Pcoq.G.Symbol.opt %a)" print_symbol s
+ fprintf fmt "(Pcoq.Symbol.opt %a)" print_symbol s
| SymbRules rules ->
let pr fmt (r, body) =
let (vars, tkn) = List.split r in
let tkn = List.rev tkn in
- fprintf fmt "Pcoq.G.Rules.make @[(%a)@ (%a)@]" (print_symbols ~norec:true) tkn print_fun (vars, body)
+ fprintf fmt "Pcoq.Rules.make @[(%a)@ (%a)@]" (print_symbols ~norec:true) tkn print_fun (vars, body)
in
let pr fmt rules = print_list fmt pr rules in
- fprintf fmt "(Pcoq.G.Symbol.rules %a)" pr (List.rev rules)
+ fprintf fmt "(Pcoq.Symbol.rules %a)" pr (List.rev rules)
| SymbQuote c ->
fprintf fmt "(%s)" c
@@ -266,7 +266,7 @@ let print_rule fmt r =
let print_entry fmt e =
let print_position_opt fmt pos = print_opt fmt print_position pos in
let print_rules fmt rules = print_list fmt print_rule rules in
- fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ @[{ Pcoq.G.pos=%a; data=%a}@]@]@ in@ "
+ fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ @[{ Pcoq.pos=%a; data=%a}@]@]@ in@ "
e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules
let print_ast fmt ext =
@@ -452,7 +452,7 @@ let terminal s =
let p =
if s <> "" && s.[0] >= '0' && s.[0] <= '9' then "CLexer.terminal_numeral"
else "CLexer.terminal" in
- let c = Printf.sprintf "Pcoq.G.Symbol.token (%s \"%s\")" p s in
+ let c = Printf.sprintf "Pcoq.Symbol.token (%s \"%s\")" p s in
SymbQuote c
let rec parse_symb self = function
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 834850082e..41669b77c9 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -26,6 +26,7 @@ module type S = sig
module Entry : sig
type 'a t
val make : string -> 'a t
+ val create : string -> 'a t
val parse : 'a t -> Parsable.t -> 'a
val name : 'a t -> string
val of_parser : string -> (Plexing.location_function -> te Stream.t -> 'a) -> 'a t
@@ -1578,6 +1579,7 @@ module Entry = struct
econtinue =
(fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure);
edesc = Dlevels []}
+ let create = make
let parse (e : 'a t) p : 'a =
Parsable.parse_parsable e p
let parse_token_stream (e : 'a t) ts : 'a =
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 0872321da0..6f998f7b80 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -36,6 +36,7 @@ module type S = sig
module Entry : sig
type 'a t
val make : string -> 'a t
+ val create : string -> 'a t (* compat *)
val parse : 'a t -> Parsable.t -> 'a
val name : 'a t -> string
val of_parser : string -> (Plexing.location_function -> te Stream.t -> 'a) -> 'a t
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 81e7e4d148..0ef7fca41f 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -91,7 +91,7 @@ let set_doc doc = ide_doc := Some doc
let add ((s,eid),(sid,verbose)) =
let doc = get_doc () in
- let pa = Pcoq.G.Parsable.make (Stream.of_string s) in
+ let pa = Pcoq.Parsable.make (Stream.of_string s) in
match Stm.parse_sentence ~doc sid ~entry:Pvernac.main_entry pa with
| None -> assert false (* s is not an empty string *)
| Some ast ->
@@ -127,13 +127,13 @@ let edit_at id =
* be removed in the next version of the protocol.
*)
let query (route, (s,id)) =
- let pa = Pcoq.G.Parsable.make (Stream.of_string s) in
+ let pa = Pcoq.Parsable.make (Stream.of_string s) in
let doc = get_doc () in
Stm.query ~at:id ~doc ~route pa
let annotate phrase =
let doc = get_doc () in
- let pa = Pcoq.G.Parsable.make (Stream.of_string phrase) in
+ let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
match Stm.parse_sentence ~doc (Stm.get_current_state ~doc) ~entry:Pvernac.main_entry pa with
| None -> Richpp.richpp_of_pp 78 (Pp.mt ())
| Some ast ->
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index fe280c1f69..5b0562fb0d 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -14,12 +14,7 @@ open Genarg
open Gramlib
(** The parser of Coq *)
-module G = Grammar.GMake(CLexer.Lexer)
-
-module Entry = struct
- include G.Entry
- let create = make
-end
+include Grammar.GMake(CLexer.Lexer)
module Lookahead =
struct
@@ -40,7 +35,7 @@ struct
let to_entry s (lk : t) =
let run tok strm = match lk tok 0 strm with None -> err () | Some _ -> () in
- G.Entry.of_parser s run
+ Entry.of_parser s run
let (>>) (lk1 : t) lk2 tok n strm = match lk1 tok n strm with
| None -> None
@@ -94,17 +89,17 @@ end
type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
type extend_rule =
-| ExtendRule : 'a G.Entry.t * 'a G.extend_statement -> extend_rule
-| ExtendRuleReinit : 'a G.Entry.t * gram_reinit * 'a G.extend_statement -> extend_rule
+| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
+| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule
module EntryCommand = Dyn.Make ()
-module EntryData = struct type _ t = Ex : 'b G.Entry.t String.Map.t -> ('a * 'b) t end
+module EntryData = struct type _ t = Ex : 'b Entry.t String.Map.t -> ('a * 'b) t end
module EntryDataMap = EntryCommand.Map(EntryData)
type ext_kind =
| ByGrammar of extend_rule
| ByEXTEND of (unit -> unit) * (unit -> unit)
- | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.Entry.t -> ext_kind
+ | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b Entry.t -> ext_kind
(** The list of extensions *)
@@ -114,37 +109,37 @@ let camlp5_entries = ref EntryDataMap.empty
(** Deletion *)
-let grammar_delete e { G.pos; data } =
+let grammar_delete e { pos; data } =
List.iter
(fun (n,ass,lev) ->
- List.iter (fun pil -> G.safe_delete_rule e pil) (List.rev lev))
+ List.iter (fun pil -> safe_delete_rule e pil) (List.rev lev))
(List.rev data)
-let grammar_delete_reinit e reinit ({ G.pos; data } as d)=
+let grammar_delete_reinit e reinit ({ pos; data } as d)=
grammar_delete e d;
let a, ext = reinit in
let lev = match pos with
| Some (Gramext.Level n) -> n
| _ -> assert false
in
- let ext = { G.pos = Some ext; data = [Some lev,Some a,[]] } in
- G.safe_extend e ext
+ let ext = { pos = Some ext; data = [Some lev,Some a,[]] } in
+ safe_extend e ext
(** Extension *)
let grammar_extend e ext =
let undo () = grammar_delete e ext in
- let redo () = G.safe_extend e ext in
+ let redo () = safe_extend e ext in
camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state;
redo ()
let grammar_extend_sync e ext =
camlp5_state := ByGrammar (ExtendRule (e, ext)) :: !camlp5_state;
- G.safe_extend e ext
+ safe_extend e ext
let grammar_extend_sync_reinit e reinit ext =
camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state;
- G.safe_extend e ext
+ safe_extend e ext
(** Remove extensions
@@ -170,7 +165,7 @@ let rec remove_grammars n =
redo();
camlp5_state := ByEXTEND (undo,redo) :: !camlp5_state
| ByEntry (tag, name, e) :: t ->
- G.Unsafe.clear_entry e;
+ Unsafe.clear_entry e;
camlp5_state := t;
let EntryData.Ex entries =
try EntryDataMap.find tag !camlp5_entries
@@ -185,19 +180,19 @@ let make_rule r = [None, None, r]
(** An entry that checks we reached the end of the input. *)
let eoi_entry en =
- let e = G.Entry.make ((G.Entry.name en) ^ "_eoi") in
- let symbs = G.Rule.next (G.Rule.next G.Rule.stop (G.Symbol.nterm en)) (G.Symbol.token Tok.PEOI) in
+ let e = Entry.make ((Entry.name en) ^ "_eoi") in
+ let symbs = Rule.next (Rule.next Rule.stop (Symbol.nterm en)) (Symbol.token Tok.PEOI) in
let act = fun _ x loc -> x in
- let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in
- G.safe_extend e ext;
+ let ext = { pos = None; data = make_rule [Production.make symbs act] } in
+ safe_extend e ext;
e
let map_entry f en =
- let e = G.Entry.make ((G.Entry.name en) ^ "_map") in
- let symbs = G.Rule.next G.Rule.stop (G.Symbol.nterm en) in
+ let e = Entry.make ((Entry.name en) ^ "_map") in
+ let symbs = Rule.next Rule.stop (Symbol.nterm en) in
let act = fun x loc -> f x in
- let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in
- G.safe_extend e ext;
+ let ext = { pos = None; data = make_rule [Production.make symbs act] } in
+ safe_extend e ext;
e
(* Parse a string, does NOT check if the entire string was read
@@ -205,7 +200,7 @@ let map_entry f en =
let parse_string f ?loc x =
let strm = Stream.of_string x in
- G.Entry.parse f (G.Parsable.make ?loc strm)
+ Entry.parse f (Parsable.make ?loc strm)
type gram_universe = string
@@ -226,14 +221,14 @@ let get_univ u =
let new_entry u s =
let ename = u ^ ":" ^ s in
- let e = G.Entry.make ename in
+ let e = Entry.make ename in
e
let make_gen_entry u s = new_entry u s
module GrammarObj =
struct
- type ('r, _, _) obj = 'r G.Entry.t
+ type ('r, _, _) obj = 'r Entry.t
let name = "grammar"
let default _ = None
end
@@ -256,7 +251,7 @@ 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 G.Entry.t =
+let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Entry.t =
let e = new_entry u s in
let Rawwit t = etyp in
let () = Grammar.register0 t e in
@@ -342,11 +337,11 @@ module Module =
let module_type = Entry.create "module_type"
end
-let epsilon_value (type s tr a) f (e : (s, tr, a) G.Symbol.t) =
- let r = G.Production.make (G.Rule.next G.Rule.stop e) (fun x _ -> f x) in
- let entry = G.Entry.make "epsilon" in
- let ext = { G.pos = None; data = [None, None, [r]] } in
- let () = G.safe_extend entry ext in
+let epsilon_value (type s tr a) f (e : (s, tr, a) Symbol.t) =
+ let r = Production.make (Rule.next Rule.stop e) (fun x _ -> f x) in
+ let entry = Entry.make "epsilon" in
+ let ext = { pos = None; data = [None, None, [r]] } in
+ let () = safe_extend entry ext in
try Some (parse_string entry "") with _ -> None
(** Synchronized grammar extensions *)
@@ -404,14 +399,14 @@ let extend_grammar_command tag g =
let nb = List.length rules in
grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack
-let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b G.Entry.t list =
+let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Entry.t list =
let EntryInterp.Ex modify = EntryInterpMap.find tag !entry_interp in
let grammar_state = match !grammar_stack with
| [] -> GramState.empty
| (_, st) :: _ -> st
in
let (names, st) = modify g grammar_state in
- let entries = List.map (fun name -> G.Entry.make name) names in
+ let entries = List.map (fun name -> Entry.make name) names in
let iter name e =
camlp5_state := ByEntry (tag, name, e) :: !camlp5_state;
let EntryData.Ex old =
@@ -437,7 +432,7 @@ let extend_dyn_grammar (e, _) = match e with
(** Registering extra grammar *)
-type any_entry = AnyEntry : 'a G.Entry.t -> any_entry
+type any_entry = AnyEntry : 'a Entry.t -> any_entry
let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 5d21b39dee..90088be307 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -15,14 +15,7 @@ open Libnames
(** The parser of Coq *)
-module G : Gramlib.Grammar.S with type te = Tok.t and type 'a pattern = 'a Tok.p
-
-(** Compatibility module, please avoid *)
-module Entry : sig
- type 'a t = 'a G.Entry.t
- val create : string -> 'a t
- val of_parser : string -> (Gramlib.Plexing.location_function -> Tok.t Stream.t -> 'a) -> 'a t
-end
+include Gramlib.Grammar.S with type te = Tok.t and type 'a pattern = 'a Tok.p
module Lookahead : sig
type t
@@ -214,11 +207,11 @@ module Module :
(** {5 Type-safe grammar extension} *)
-val epsilon_value : ('a -> 'self) -> ('self, _, 'a) G.Symbol.t -> 'self option
+val epsilon_value : ('a -> 'self) -> ('self, _, 'a) Symbol.t -> 'self option
(** {5 Extending the parser without synchronization} *)
-val grammar_extend : 'a Entry.t -> 'a G.extend_statement -> unit
+val grammar_extend : 'a Entry.t -> 'a extend_statement -> unit
(** Extend the grammar of Coq, without synchronizing it with the backtracking
mechanism. This means that grammar extensions defined this way will survive
an undo. *)
@@ -238,8 +231,8 @@ type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
(** Type of reinitialization data *)
type extend_rule =
-| ExtendRule : 'a Entry.t * 'a G.extend_statement -> extend_rule
-| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a G.extend_statement -> extend_rule
+| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
+| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule
type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t
(** Grammar extension entry point. Given some ['a] and a current grammar state,
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index bec83411c1..5a26ac8827 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -62,7 +62,7 @@ open Extraargs
(* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
let check_for_coloneq =
- Pcoq.G.Entry.of_parser "lpar_id_colon"
+ Pcoq.Entry.of_parser "lpar_id_colon"
(fun _ strm ->
let rec skip_to_rpar p n =
match List.last (Stream.npeek n strm) with
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index eed7f07b2e..4127d28bae 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -44,11 +44,11 @@ let coincide s pat off =
!break
let atactic n =
- if n = 5 then Pcoq.G.Symbol.nterm Pltac.binder_tactic
- else Pcoq.G.Symbol.nterml Pltac.tactic_expr (string_of_int n)
+ if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic
+ else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n)
type entry_name = EntryName :
- 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.G.Symbol.t -> entry_name
+ 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.Symbol.t -> entry_name
(** Quite ad-hoc *)
let get_tacentry n m =
@@ -57,8 +57,8 @@ let get_tacentry n m =
&& not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
&& not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
in
- if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Pcoq.G.Symbol.self)
- else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Pcoq.G.Symbol.next)
+ if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Pcoq.Symbol.self)
+ else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Pcoq.Symbol.next)
else EntryName (rawwit Tacarg.wit_tactic, atactic n)
let get_separator = function
@@ -140,23 +140,23 @@ let head_is_ident tg = match tg.tacgram_prods with
let rec prod_item_of_symbol lev = function
| Extend.Ulist1 s ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list1 e)
+ EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list1 e)
| Extend.Ulist0 s ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list0 e)
+ EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list0 e)
| Extend.Ulist1sep (s, sep) ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list1sep e (Pcoq.G.Symbol.token (CLexer.terminal sep)) false)
+ EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list1sep e (Pcoq.Symbol.token (CLexer.terminal sep)) false)
| Extend.Ulist0sep (s, sep) ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list0sep e (Pcoq.G.Symbol.token (CLexer.terminal sep)) false)
+ EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list0sep e (Pcoq.Symbol.token (CLexer.terminal sep)) false)
| Extend.Uopt s ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (OptArg typ), Pcoq.G.Symbol.opt e)
+ EntryName (Rawwit (OptArg typ), Pcoq.Symbol.opt e)
| Extend.Uentry arg ->
let ArgT.Any tag = arg in
let wit = ExtraArg tag in
- EntryName (Rawwit wit, Pcoq.G.Symbol.nterm (genarg_grammar wit))
+ EntryName (Rawwit wit, Pcoq.Symbol.nterm (genarg_grammar wit))
| Extend.Uentryl (s, n) ->
let ArgT.Any tag = s in
assert (coincide (ArgT.repr tag) "tactic" 0);
@@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) state =
in
let prods = List.map map tg.tacgram_prods in
let rules = make_rule mkact prods in
- let r = ExtendRule (entry, { G.pos; data=[(None, None, [rules])]}) in
+ let r = ExtendRule (entry, { pos; data=[(None, None, [rules])]}) in
([r], state)
let tactic_grammar =
@@ -399,14 +399,14 @@ let create_ltac_quotation name cast (e, l) =
in
let () = ltac_quotations := String.Set.add name !ltac_quotations in
let entry = match l with
- | None -> Pcoq.G.Symbol.nterm e
- | Some l -> Pcoq.G.Symbol.nterml e (string_of_int l)
+ | None -> Pcoq.Symbol.nterm e
+ | Some l -> Pcoq.Symbol.nterml e (string_of_int l)
in
(* let level = Some "1" in *)
let level = None in
let assoc = None in
let rule =
- Pcoq.G.(
+ Pcoq.(
Rule.next
(Rule.next
(Rule.next
@@ -420,8 +420,8 @@ let create_ltac_quotation name cast (e, l) =
(Symbol.token (CLexer.terminal ")")))
in
let action _ v _ _ _ loc = cast (Some loc, v) in
- let gram = (level, assoc, [Pcoq.G.Production.make rule action]) in
- Pcoq.grammar_extend Pltac.tactic_arg {G.pos=None; data=[gram]}
+ let gram = (level, assoc, [Pcoq.Production.make rule action]) in
+ Pcoq.grammar_extend Pltac.tactic_arg {pos=None; data=[gram]}
(** Command *)
@@ -765,7 +765,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
e
| Vernacextend.Arg_rules rules ->
let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
- let () = Pcoq.grammar_extend e {G.pos=None; data=[(None, None, rules)]} in
+ let () = Pcoq.grammar_extend e {pos=None; data=[(None, None, rules)]} in
e
in
let (rpr, gpr, tpr) = arg.arg_printer in
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index c3396584a4..442b40221b 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -263,16 +263,16 @@ let negate_parser f tok x =
| Some _ -> raise Stream.Failure
let test_not_ssrslashnum =
- Pcoq.G.Entry.of_parser
+ Pcoq.Entry.of_parser
"test_not_ssrslashnum" (negate_parser test_ssrslashnum10)
let test_ssrslashnum00 =
- Pcoq.G.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00
+ Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00
let test_ssrslashnum10 =
- Pcoq.G.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10
+ Pcoq.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10
let test_ssrslashnum11 =
- Pcoq.G.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11
+ Pcoq.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11
let test_ssrslashnum01 =
- Pcoq.G.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01
+ Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01
}
@@ -459,7 +459,7 @@ let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
| Tok.KEYWORD "@" -> xWithAt
| _ -> xNoFlag
-let ssrtermkind = Pcoq.G.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
(* New kinds of terms *)
@@ -470,7 +470,7 @@ let input_term_annotation _ strm =
| Tok.KEYWORD "@" :: _ -> `At
| _ -> `None
let term_annotation =
- Pcoq.G.Entry.of_parser "term_annotation" input_term_annotation
+ Pcoq.Entry.of_parser "term_annotation" input_term_annotation
(* terms *)
@@ -811,7 +811,7 @@ let reject_ssrhid _ strm =
| _ -> ())
| _ -> ()
-let test_nohidden = Pcoq.G.Entry.of_parser "test_ssrhid" reject_ssrhid
+let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid
let rec reject_binder crossed_paren k tok s =
match
@@ -825,7 +825,7 @@ let rec reject_binder crossed_paren k tok s =
| Some (Tok.KEYWORD ")") when crossed_paren -> raise Stream.Failure
| _ -> if crossed_paren then () else raise Stream.Failure
-let _test_nobinder = Pcoq.G.Entry.of_parser "test_nobinder" (reject_binder false 0)
+let _test_nobinder = Pcoq.Entry.of_parser "test_nobinder" (reject_binder false 0)
}
@@ -1659,7 +1659,7 @@ let ssr_id_of_string loc s =
^ "Scripts with explicit references to anonymous variables are fragile."))
end; Id.of_string s
-let ssr_null_entry = Pcoq.G.Entry.of_parser "ssr_null" (fun _ _ -> ())
+let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ _ -> ())
}
@@ -2382,7 +2382,7 @@ let test_ssr_rw_syntax =
match Util.stream_nth 0 strm with
| Tok.KEYWORD key when List.mem key.[0] [lbrace; '['; '/'] -> ()
| _ -> raise Stream.Failure in
- Pcoq.G.Entry.of_parser "test_ssr_rw_syntax" test
+ Pcoq.Entry.of_parser "test_ssr_rw_syntax" test
}
diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg
index 59abf80dc5..33e523a4a4 100644
--- a/plugins/ssrmatching/g_ssrmatching.mlg
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -70,7 +70,7 @@ let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
| Tok.KEYWORD "(" -> '('
| Tok.KEYWORD "@" -> '@'
| _ -> ' '
-let ssrtermkind = Pcoq.G.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
}
diff --git a/stm/stm.mli b/stm/stm.mli
index 88da3c747f..2c27d63b82 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -93,7 +93,7 @@ val new_doc : stm_init_options -> doc * Stateid.t
be the case if an error was raised at parsing time). *)
val parse_sentence :
doc:doc -> Stateid.t ->
- entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.G.Parsable.t -> 'a
+ entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.Parsable.t -> 'a
(* Reminder: A parsable [pa] is constructed using
[Pcoq.Parsable.t stream], where [stream : char Stream.t]. *)
@@ -119,7 +119,7 @@ val get_proof : doc:doc -> Stateid.t -> Proof.t option
throwing away side effects except messages. Feedback will
be sent with [report_with], which defaults to the dummy state id *)
val query : doc:doc ->
- at:Stateid.t -> route:Feedback.route_id -> Pcoq.G.Parsable.t -> unit
+ at:Stateid.t -> route:Feedback.route_id -> Pcoq.Parsable.t -> unit
(* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if
the requested id is the new document tip hence the document portion following
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 0d9edb248b..b8acdd3af1 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -23,7 +23,7 @@ type input_buffer = {
mutable str : Bytes.t; (* buffer of already read characters *)
mutable len : int; (* number of chars in the buffer *)
mutable bols : int list; (* offsets in str of beginning of lines *)
- mutable tokens : Pcoq.G.Parsable.t; (* stream of tokens *)
+ mutable tokens : Pcoq.Parsable.t; (* stream of tokens *)
mutable start : int } (* stream count of the first char of the buffer *)
(* Double the size of the buffer. *)
@@ -76,7 +76,7 @@ let reset_input_buffer doc ic ibuf =
ibuf.str <- Bytes.empty;
ibuf.len <- 0;
ibuf.bols <- [];
- ibuf.tokens <- Pcoq.G.Parsable.make (Stream.from (prompt_char doc ic ibuf));
+ ibuf.tokens <- Pcoq.Parsable.make (Stream.from (prompt_char doc ic ibuf));
ibuf.start <- 0
(* Functions to print underlined locations from an input buffer. *)
@@ -230,7 +230,7 @@ let top_buffer =
str = Bytes.empty;
len = 0;
bols = [];
- tokens = Pcoq.G.Parsable.make (Stream.of_list []);
+ tokens = Pcoq.Parsable.make (Stream.of_list []);
start = 0 }
let set_prompt prompt =
@@ -247,7 +247,7 @@ let parse_to_dot =
| Tok.EOI -> ()
| _ -> dot tok st
in
- Pcoq.G.Entry.of_parser "Coqtoplevel.dot" dot
+ Pcoq.Entry.of_parser "Coqtoplevel.dot" dot
(* If an error occurred while parsing, we try to read the input until a dot
token is encountered.
@@ -255,7 +255,7 @@ let parse_to_dot =
let rec discard_to_dot () =
try
- Pcoq.G.Entry.parse parse_to_dot top_buffer.tokens
+ Pcoq.Entry.parse parse_to_dot top_buffer.tokens
with
| CLexer.Error.E _ -> discard_to_dot ()
| e when CErrors.noncritical e -> ()
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index b07f3e5c57..1eafc70530 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -18,7 +18,7 @@ type input_buffer = {
mutable str : Bytes.t; (** buffer of already read characters *)
mutable len : int; (** number of chars in the buffer *)
mutable bols : int list; (** offsets in str of beginning of lines *)
- mutable tokens : Pcoq.G.Parsable.t; (** stream of tokens *)
+ mutable tokens : Pcoq.Parsable.t; (** stream of tokens *)
mutable start : int } (** stream count of the first char of the buffer *)
(** The input buffer of stdin. *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f501e89ed5..076796468f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -88,7 +88,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in
let in_pa =
- Pcoq.G.Parsable.make ~loc:(Loc.initial (Loc.InFile file))
+ Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile file))
(Stream.of_channel in_chan) in
let open State in
@@ -100,7 +100,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
with
| None ->
input_cleanup ();
- state, ids, Pcoq.G.Parsable.comments in_pa
+ state, ids, Pcoq.Parsable.comments in_pa
| Some ast ->
(* Printing of AST for -compile-verbose *)
Option.iter (vernac_echo ?loc:ast.CAst.loc) in_echo;
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 477672ebdb..57d59fc2ef 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -827,9 +827,9 @@ END
let () =
let open Tok in
-let (++) r s = Pcoq.G.Rule.next r s in
+let (++) r s = Pcoq.Rule.next r s in
let rules = [
- Pcoq.G.(
+ Pcoq.(
Production.make
(Rule.stop ++ Symbol.nterm test_dollar_ident ++ Symbol.token (PKEYWORD "$") ++ Symbol.nterm Prim.ident)
begin fun id _ _ loc ->
@@ -839,7 +839,7 @@ let rules = [
end
);
- Pcoq.G.(
+ Pcoq.(
Production.make
(Rule.stop ++ Symbol.nterm test_ampersand_ident ++ Symbol.token (PKEYWORD "&") ++ Symbol.nterm Prim.ident)
begin fun id _ _ loc ->
@@ -849,7 +849,7 @@ let rules = [
end
);
- Pcoq.G.(
+ Pcoq.(
Production.make
(Rule.stop ++ Symbol.token (PIDENT (Some "ltac2")) ++ Symbol.token (PKEYWORD ":") ++
Symbol.token (PKEYWORD "(") ++ Symbol.nterm tac2expr ++ Symbol.token (PKEYWORD ")"))
@@ -861,7 +861,7 @@ let rules = [
] in
Hook.set Tac2entries.register_constr_quotations begin fun () ->
- Pcoq.grammar_extend Pcoq.Constr.operconstr {G.pos=Some (Gramlib.Gramext.Level "0"); data=[(None, None, rules)]}
+ Pcoq.grammar_extend Pcoq.Constr.operconstr {pos=Some (Gramlib.Gramext.Level "0"); data=[(None, None, rules)]}
end
}
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index ab660b486e..2ed854c9f7 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1431,7 +1431,7 @@ let q_unit = CAst.make @@ CTacCst (AbsKn (Tuple 0))
let add_generic_scope s entry arg =
let parse = function
| [] ->
- let scope = Pcoq.G.Symbol.nterm entry in
+ let scope = Pcoq.Symbol.nterm entry in
let act x = CAst.make @@ CTacExt (arg, x) in
Tac2entries.ScopeRule (scope, act)
| arg -> scope_fail s arg
@@ -1442,14 +1442,14 @@ open CAst
let () = add_scope "keyword" begin function
| [SexprStr {loc;v=s}] ->
- let scope = Pcoq.G.Symbol.token (Tok.PKEYWORD s) in
+ let scope = Pcoq.Symbol.token (Tok.PKEYWORD s) in
Tac2entries.ScopeRule (scope, (fun _ -> q_unit))
| arg -> scope_fail "keyword" arg
end
let () = add_scope "terminal" begin function
| [SexprStr {loc;v=s}] ->
- let scope = Pcoq.G.Symbol.token (CLexer.terminal s) in
+ let scope = Pcoq.Symbol.token (CLexer.terminal s) in
Tac2entries.ScopeRule (scope, (fun _ -> q_unit))
| arg -> scope_fail "terminal" arg
end
@@ -1457,13 +1457,13 @@ end
let () = add_scope "list0" begin function
| [tok] ->
let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
- let scope = Pcoq.G.Symbol.list0 scope in
+ let scope = Pcoq.Symbol.list0 scope in
let act l = Tac2quote.of_list act l in
Tac2entries.ScopeRule (scope, act)
| [tok; SexprStr {v=str}] ->
let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
- let sep = Pcoq.G.Symbol.token (CLexer.terminal str) in
- let scope = Pcoq.G.Symbol.list0sep scope sep false in
+ let sep = Pcoq.Symbol.token (CLexer.terminal str) in
+ let scope = Pcoq.Symbol.list0sep scope sep false in
let act l = Tac2quote.of_list act l in
Tac2entries.ScopeRule (scope, act)
| arg -> scope_fail "list0" arg
@@ -1472,13 +1472,13 @@ end
let () = add_scope "list1" begin function
| [tok] ->
let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
- let scope = Pcoq.G.Symbol.list1 scope in
+ let scope = Pcoq.Symbol.list1 scope in
let act l = Tac2quote.of_list act l in
Tac2entries.ScopeRule (scope, act)
| [tok; SexprStr {v=str}] ->
let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
- let sep = Pcoq.G.Symbol.token (CLexer.terminal str) in
- let scope = Pcoq.G.Symbol.list1sep scope sep false in
+ let sep = Pcoq.Symbol.token (CLexer.terminal str) in
+ let scope = Pcoq.Symbol.list1sep scope sep false in
let act l = Tac2quote.of_list act l in
Tac2entries.ScopeRule (scope, act)
| arg -> scope_fail "list1" arg
@@ -1487,7 +1487,7 @@ end
let () = add_scope "opt" begin function
| [tok] ->
let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
- let scope = Pcoq.G.Symbol.opt scope in
+ let scope = Pcoq.Symbol.opt scope in
let act opt = match opt with
| None ->
CAst.make @@ CTacCst (AbsKn (Other Core.c_none))
@@ -1500,7 +1500,7 @@ end
let () = add_scope "self" begin function
| [] ->
- let scope = Pcoq.G.Symbol.self in
+ let scope = Pcoq.Symbol.self in
let act tac = tac in
Tac2entries.ScopeRule (scope, act)
| arg -> scope_fail "self" arg
@@ -1508,7 +1508,7 @@ end
let () = add_scope "next" begin function
| [] ->
- let scope = Pcoq.G.Symbol.next in
+ let scope = Pcoq.Symbol.next in
let act tac = tac in
Tac2entries.ScopeRule (scope, act)
| arg -> scope_fail "next" arg
@@ -1517,12 +1517,12 @@ end
let () = add_scope "tactic" begin function
| [] ->
(* Default to level 5 parsing *)
- let scope = Pcoq.G.Symbol.nterml tac2expr "5" in
+ let scope = Pcoq.Symbol.nterml tac2expr "5" in
let act tac = tac in
Tac2entries.ScopeRule (scope, act)
| [SexprInt {loc;v=n}] as arg ->
let () = if n < 0 || n > 6 then scope_fail "tactic" arg in
- let scope = Pcoq.G.Symbol.nterml tac2expr (string_of_int n) in
+ let scope = Pcoq.Symbol.nterml tac2expr (string_of_int n) in
let act tac = tac in
Tac2entries.ScopeRule (scope, act)
| arg -> scope_fail "tactic" arg
@@ -1543,12 +1543,12 @@ let () = add_scope "constr" (fun arg ->
arg
in
let act e = Tac2quote.of_constr ~delimiters e in
- Tac2entries.ScopeRule (Pcoq.G.Symbol.nterm Pcoq.Constr.constr, act)
+ Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act)
)
let add_expr_scope name entry f =
add_scope name begin function
- | [] -> Tac2entries.ScopeRule (Pcoq.G.Symbol.nterm entry, f)
+ | [] -> Tac2entries.ScopeRule (Pcoq.Symbol.nterm entry, f)
| arg -> scope_fail name arg
end
@@ -1590,21 +1590,21 @@ let rec apply : type a. a converter -> raw_tacexpr list -> a = function
| CvCns (c, Some f) -> fun accu x -> apply c (f x :: accu)
type seqrule =
-| Seqrule : (Tac2expr.raw_tacexpr, Gramlib.Grammar.norec, 'act, Loc.t -> raw_tacexpr) G.Rule.t * 'act converter -> seqrule
+| Seqrule : (Tac2expr.raw_tacexpr, Gramlib.Grammar.norec, 'act, Loc.t -> raw_tacexpr) Rule.t * 'act converter -> seqrule
let rec make_seq_rule = function
| [] ->
- Seqrule (Pcoq.G.Rule.stop, CvNil)
+ Seqrule (Pcoq.Rule.stop, CvNil)
| tok :: rem ->
let Tac2entries.ScopeRule (scope, f) = Tac2entries.parse_scope tok in
let scope =
- match Pcoq.G.generalize_symbol scope with
+ match Pcoq.generalize_symbol scope with
| None ->
CErrors.user_err (str "Recursive symbols (self / next) are not allowed in local rules")
| Some scope -> scope
in
let Seqrule (r, c) = make_seq_rule rem in
- let r = Pcoq.G.Rule.next_norec r scope in
+ let r = Pcoq.Rule.next_norec r scope in
let f = match tok with
| SexprStr _ -> None (* Leave out mere strings *)
| _ -> Some f
@@ -1614,7 +1614,7 @@ let rec make_seq_rule = function
let () = add_scope "seq" begin fun toks ->
let scope =
let Seqrule (r, c) = make_seq_rule (List.rev toks) in
- Pcoq.G.(Symbol.rules [Rules.make r (apply c [])])
+ Pcoq.(Symbol.rules [Rules.make r (apply c [])])
in
Tac2entries.ScopeRule (scope, (fun e -> e))
end
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 7c4971db8c..ebc63ddd01 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -558,7 +558,7 @@ type 'a token =
| TacNonTerm of Name.t * 'a
type scope_rule =
-| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.G.Symbol.t * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.Symbol.t * ('a -> raw_tacexpr) -> scope_rule
type scope_interpretation = sexpr list -> scope_rule
@@ -583,7 +583,7 @@ let parse_scope = function
CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Names.Id.print id)
| SexprStr {v=str} ->
let v_unit = CAst.make @@ CTacCst (AbsKn (Tuple 0)) in
- ScopeRule (Pcoq.G.Symbol.token (Tok.PIDENT (Some str)), (fun _ -> v_unit))
+ ScopeRule (Pcoq.Symbol.token (Tok.PIDENT (Some str)), (fun _ -> v_unit))
| tok ->
let loc = loc_of_token tok in
CErrors.user_err ?loc (str "Invalid parsing token")
@@ -611,19 +611,19 @@ type synext = {
type krule =
| KRule :
- (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Pcoq.G.Rule.t *
+ (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Pcoq.Rule.t *
((Loc.t -> (Name.t * raw_tacexpr) list -> raw_tacexpr) -> 'act) -> krule
let rec get_rule (tok : scope_rule token list) : krule = match tok with
-| [] -> KRule (Pcoq.G.Rule.stop, fun k loc -> k loc [])
+| [] -> KRule (Pcoq.Rule.stop, fun k loc -> k loc [])
| TacNonTerm (na, ScopeRule (scope, inj)) :: tok ->
let KRule (rule, act) = get_rule tok in
- let rule = Pcoq.G.Rule.next rule scope in
+ let rule = Pcoq.Rule.next rule scope in
let act k e = act (fun loc acc -> k loc ((na, inj e) :: acc)) in
KRule (rule, act)
| TacTerm t :: tok ->
let KRule (rule, act) = get_rule tok in
- let rule = Pcoq.G.(Rule.next rule (Symbol.token (CLexer.terminal t))) in
+ let rule = Pcoq.(Rule.next rule (Symbol.token (CLexer.terminal t))) in
let act k _ = act k in
KRule (rule, act)
@@ -637,13 +637,13 @@ let perform_notation syn st =
let bnd = List.map map args in
CAst.make ~loc @@ CTacLet (false, bnd, syn.synext_exp)
in
- let rule = Pcoq.G.Production.make rule (act mk) in
+ let rule = Pcoq.Production.make rule (act mk) in
let lev = match syn.synext_lev with
| None -> None
| Some lev -> Some (string_of_int lev)
in
let rule = (lev, None, [rule]) in
- ([Pcoq.ExtendRule (Pltac.tac2expr, {Pcoq.G.pos=None; data=[rule]})], st)
+ ([Pcoq.ExtendRule (Pltac.tac2expr, {Pcoq.pos=None; data=[rule]})], st)
let ltac2_notation =
Pcoq.create_grammar_command "ltac2-notation" perform_notation
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index 1efac697aa..edad118dc9 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -36,7 +36,7 @@ val perform_eval : pstate:Proof_global.t option -> raw_tacexpr -> unit
(** {5 Notations} *)
type scope_rule =
-| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.G.Symbol.t * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.Symbol.t * ('a -> raw_tacexpr) -> scope_rule
type scope_interpretation = sexpr list -> scope_rule
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index c4f15a40ce..fdc8b1ba4c 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -326,47 +326,47 @@ let is_binder_level custom (custom',from) e = match e with
let make_sep_rules = function
| [tk] ->
- Pcoq.G.Symbol.token tk
+ Pcoq.Symbol.token tk
| tkl ->
- let r = Pcoq.G.mk_rule (List.rev tkl) in
- Pcoq.G.Symbol.rules [r]
+ let r = Pcoq.mk_rule (List.rev tkl) in
+ Pcoq.Symbol.rules [r]
type ('s, 'a) mayrec_symbol =
-| MayRecNo : ('s, Gramlib.Grammar.norec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol
-| MayRecMay : ('s, Gramlib.Grammar.mayrec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol
+| MayRecNo : ('s, Gramlib.Grammar.norec, 'a) Symbol.t -> ('s, 'a) mayrec_symbol
+| MayRecMay : ('s, Gramlib.Grammar.mayrec, 'a) Symbol.t -> ('s, 'a) mayrec_symbol
let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat ->
if is_binder_level custom from p
then
(* Prevent self *)
- MayRecNo (Pcoq.G.Symbol.nterml (target_entry custom forpat) "200")
- else if is_self custom from p then MayRecMay Pcoq.G.Symbol.self
+ MayRecNo (Pcoq.Symbol.nterml (target_entry custom forpat) "200")
+ else if is_self custom from p then MayRecMay Pcoq.Symbol.self
else
let g = target_entry custom forpat in
let lev = adjust_level custom assoc from p in
begin match lev with
- | DefaultLevel -> MayRecNo (Pcoq.G.Symbol.nterm g)
- | NextLevel -> MayRecMay Pcoq.G.Symbol.next
- | NumLevel lev -> MayRecNo (Pcoq.G.Symbol.nterml g (string_of_int lev))
+ | DefaultLevel -> MayRecNo (Pcoq.Symbol.nterm g)
+ | NextLevel -> MayRecMay Pcoq.Symbol.next
+ | NumLevel lev -> MayRecNo (Pcoq.Symbol.nterml g (string_of_int lev))
end
let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with
| TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat
| TTConstrList (s, typ', [], forpat) ->
begin match symbol_of_target s typ' assoc from forpat with
- | MayRecNo s -> MayRecNo (Pcoq.G.Symbol.list1 s)
- | MayRecMay s -> MayRecMay (Pcoq.G.Symbol.list1 s) end
+ | MayRecNo s -> MayRecNo (Pcoq.Symbol.list1 s)
+ | MayRecMay s -> MayRecMay (Pcoq.Symbol.list1 s) end
| TTConstrList (s, typ', tkl, forpat) ->
begin match symbol_of_target s typ' assoc from forpat with
- | MayRecNo s -> MayRecNo (Pcoq.G.Symbol.list1sep s (make_sep_rules tkl) false)
- | MayRecMay s -> MayRecMay (Pcoq.G.Symbol.list1sep s (make_sep_rules tkl) false) end
-| TTPattern p -> MayRecNo (Pcoq.G.Symbol.nterml Constr.pattern (string_of_int p))
-| TTClosedBinderList [] -> MayRecNo (Pcoq.G.Symbol.list1 (Pcoq.G.Symbol.nterm Constr.binder))
-| TTClosedBinderList tkl -> MayRecNo (Pcoq.G.Symbol.list1sep (Pcoq.G.Symbol.nterm Constr.binder) (make_sep_rules tkl) false)
-| TTName -> MayRecNo (Pcoq.G.Symbol.nterm Prim.name)
-| TTOpenBinderList -> MayRecNo (Pcoq.G.Symbol.nterm Constr.open_binders)
-| TTBigint -> MayRecNo (Pcoq.G.Symbol.nterm Prim.bignat)
-| TTReference -> MayRecNo (Pcoq.G.Symbol.nterm Constr.global)
+ | MayRecNo s -> MayRecNo (Pcoq.Symbol.list1sep s (make_sep_rules tkl) false)
+ | MayRecMay s -> MayRecMay (Pcoq.Symbol.list1sep s (make_sep_rules tkl) false) end
+| TTPattern p -> MayRecNo (Pcoq.Symbol.nterml Constr.pattern (string_of_int p))
+| TTClosedBinderList [] -> MayRecNo (Pcoq.Symbol.list1 (Pcoq.Symbol.nterm Constr.binder))
+| TTClosedBinderList tkl -> MayRecNo (Pcoq.Symbol.list1sep (Pcoq.Symbol.nterm Constr.binder) (make_sep_rules tkl) false)
+| TTName -> MayRecNo (Pcoq.Symbol.nterm Prim.name)
+| TTOpenBinderList -> MayRecNo (Pcoq.Symbol.nterm Constr.open_binders)
+| TTBigint -> MayRecNo (Pcoq.Symbol.nterm Prim.bignat)
+| TTReference -> MayRecNo (Pcoq.Symbol.nterm Constr.global)
let interp_entry forpat e = match e with
| ETProdName -> TTAny TTName
@@ -458,22 +458,22 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env ->
ty_eval rem f { env with constrs; constrlists; }
type ('s, 'a, 'r) mayrec_rule =
-| MayRecRNo : ('s, Gramlib.Grammar.norec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule
-| MayRecRMay : ('s, Gramlib.Grammar.mayrec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule
+| MayRecRNo : ('s, Gramlib.Grammar.norec, 'a, 'r) Rule.t -> ('s, 'a, 'r) mayrec_rule
+| MayRecRMay : ('s, Gramlib.Grammar.mayrec, 'a, 'r) Rule.t -> ('s, 'a, 'r) mayrec_rule
let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) mayrec_rule = function
-| TyStop -> MayRecRNo G.Rule.stop
+| TyStop -> MayRecRNo Rule.stop
| TyMark (_, _, _, r) -> ty_erase r
| TyNext (rem, TyTerm tok) ->
begin match ty_erase rem with
- | MayRecRNo rem -> MayRecRMay (G.Rule.next rem (G.Symbol.token tok))
- | MayRecRMay rem -> MayRecRMay (G.Rule.next rem (G.Symbol.token tok)) end
+ | MayRecRNo rem -> MayRecRMay (Rule.next rem (Symbol.token tok))
+ | MayRecRMay rem -> MayRecRMay (Rule.next rem (Symbol.token tok)) end
| TyNext (rem, TyNonTerm (_, _, s, _)) ->
begin match ty_erase rem, s with
- | MayRecRNo rem, MayRecNo s -> MayRecRMay (G.Rule.next rem s)
- | MayRecRNo rem, MayRecMay s -> MayRecRMay (G.Rule.next rem s)
- | MayRecRMay rem, MayRecNo s -> MayRecRMay (G.Rule.next rem s)
- | MayRecRMay rem, MayRecMay s -> MayRecRMay (G.Rule.next rem s) end
+ | MayRecRNo rem, MayRecNo s -> MayRecRMay (Rule.next rem s)
+ | MayRecRNo rem, MayRecMay s -> MayRecRMay (Rule.next rem s)
+ | MayRecRMay rem, MayRecNo s -> MayRecRMay (Rule.next rem s)
+ | MayRecRMay rem, MayRecMay s -> MayRecRMay (Rule.next rem s) end
type ('self, 'r) any_ty_rule =
| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
@@ -501,7 +501,7 @@ let target_to_bool : type r. r target -> bool = function
| ForPattern -> true
let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) =
- let empty = { G.pos; data = [(name, p4assoc, [])] } in
+ let empty = { pos; data = [(name, p4assoc, [])] } in
match reinit with
| None ->
ExtendRule (target_entry where forpat, empty)
@@ -520,7 +520,7 @@ let rec pure_sublevels' assoc from forpat level = function
let push where p rem =
match symbol_of_target where p assoc from forpat with
| MayRecNo sym ->
- (match Pcoq.G.level_of_nonterm sym with
+ (match Pcoq.level_of_nonterm sym with
| None -> rem
| Some i ->
if different_levels (fst from,level) (where,i) then
@@ -556,15 +556,15 @@ let extend_constr state forpat ng =
let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
let rule =
let r = match ty_erase r with
- | MayRecRNo symbs -> Pcoq.G.Production.make symbs act
- | MayRecRMay symbs -> Pcoq.G.Production.make symbs act
+ | MayRecRNo symbs -> Pcoq.Production.make symbs act
+ | MayRecRMay symbs -> Pcoq.Production.make symbs act
in
name, p4assoc, [r] in
let r = match reinit with
| None ->
- ExtendRule (entry, { G.pos; data = [rule]})
+ ExtendRule (entry, { pos; data = [rule]})
| Some reinit ->
- ExtendRuleReinit (entry, reinit, { G.pos; data = [rule]})
+ ExtendRuleReinit (entry, reinit, { pos; data = [rule]})
in
(accu @ empty_rules @ [r], state)
in
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 981de78162..bda1401bc9 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -19,13 +19,13 @@ open Vernacexpr
type 's grammar_prod_item =
| GramTerminal of string
| GramNonTerminal :
- ('a raw_abstract_argument_type * ('s, _, 'a) G.Symbol.t) Loc.located -> 's grammar_prod_item
+ ('a raw_abstract_argument_type * ('s, _, 'a) Symbol.t) Loc.located -> 's grammar_prod_item
type 'a ty_arg = ('a -> raw_generic_argument)
type ('self, 'tr, _, 'r) ty_rule =
| TyStop : ('self, Gramlib.Grammar.norec, 'r, 'r) ty_rule
-| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) G.Symbol.t * 'b ty_arg option ->
+| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Symbol.t * 'b ty_arg option ->
('self, Gramlib.Grammar.mayrec, 'b -> 'a, 'r) ty_rule
type ('self, 'r) any_ty_rule =
@@ -35,7 +35,7 @@ let rec ty_rule_of_gram = function
| [] -> AnyTyRule TyStop
| GramTerminal s :: rem ->
let AnyTyRule rem = ty_rule_of_gram rem in
- let tok = Pcoq.G.Symbol.token (CLexer.terminal s) in
+ let tok = Pcoq.Symbol.token (CLexer.terminal s) in
let r = TyNext (rem, tok, None) in
AnyTyRule r
| GramNonTerminal (_, (t, tok)) :: rem ->
@@ -44,9 +44,9 @@ let rec ty_rule_of_gram = function
let r = TyNext (rem, tok, inj) in
AnyTyRule r
-let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.G.Rule.t = function
-| TyStop -> Pcoq.G.Rule.stop
-| TyNext (rem, tok, _) -> Pcoq.G.Rule.next (ty_erase rem) tok
+let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.Rule.t = function
+| TyStop -> Pcoq.Rule.stop
+| TyNext (rem, tok, _) -> Pcoq.Rule.next (ty_erase rem) tok
type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r
@@ -62,7 +62,7 @@ let make_rule f prod =
let symb = ty_erase ty_rule in
let f loc l = f loc (List.rev l) in
let act = ty_eval ty_rule f in
- Pcoq.G.Production.make symb act
+ Pcoq.Production.make symb act
let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function
| TUentry a -> ExtraArg a
@@ -90,4 +90,4 @@ let extend_vernac_command_grammar s nt gl =
vernac_exts := (s,gl) :: !vernac_exts;
let mkact loc l = VernacExtend (s, l) in
let rules = [make_rule mkact gl] in
- grammar_extend nt { G.pos=None; data=[None, None, rules]}
+ grammar_extend nt { pos=None; data=[None, None, rules]}
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index 77198452b9..15f415ca3b 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -18,7 +18,7 @@ open Vernacexpr
type 's grammar_prod_item =
| GramTerminal of string
| GramNonTerminal : ('a Genarg.raw_abstract_argument_type *
- ('s, _, 'a) Pcoq.G.Symbol.t) Loc.located -> 's grammar_prod_item
+ ('s, _, 'a) Pcoq.Symbol.t) Loc.located -> 's grammar_prod_item
val extend_vernac_command_grammar :
extend_name -> vernac_expr Pcoq.Entry.t option ->
@@ -32,4 +32,4 @@ val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.gena
val make_rule :
(Loc.t -> Genarg.raw_generic_argument list -> 'a) ->
- 'a grammar_prod_item list -> 'a Pcoq.G.Production.t
+ 'a grammar_prod_item list -> 'a Pcoq.Production.t
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 38e57a310a..475d5c31f7 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -46,7 +46,7 @@ let entry_buf = Buffer.create 64
let pr_entry e =
let () = Buffer.clear entry_buf in
let ft = Format.formatter_of_buffer entry_buf in
- let () = Pcoq.G.Entry.print ft e in
+ let () = Pcoq.Entry.print ft e in
str (Buffer.contents entry_buf)
let pr_registered_grammar name =
@@ -55,7 +55,7 @@ let pr_registered_grammar name =
| [] -> user_err Pp.(str "Unknown or unprintable grammar entry.")
| entries ->
let pr_one (Pcoq.AnyEntry e) =
- str "Entry " ++ str (Pcoq.G.Entry.name e) ++ str " is" ++ fnl () ++
+ str "Entry " ++ str (Pcoq.Entry.name e) ++ str " is" ++ fnl () ++
pr_entry e
in
prlist pr_one entries
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 8d0dcbf0fe..2130a398e9 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -169,7 +169,7 @@ let suggest_variable env id =
let value = ref None
let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us)
-let using_from_string us = Pcoq.G.Entry.parse G_vernac.section_subset_expr (Pcoq.G.Parsable.make (Stream.of_string us))
+let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us))
let proof_using_opt_name = ["Default";"Proof";"Using"]
let () =
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 26364ed075..f4cb1adfe8 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -54,10 +54,10 @@ module Vernac_ =
let act_vernac v loc = Some v in
let act_eoi _ loc = None in
let rule = [
- Pcoq.G.(Production.make (Rule.next Rule.stop (Symbol.token Tok.PEOI)) act_eoi);
- Pcoq.G.(Production.make (Rule.next Rule.stop (Symbol.nterm vernac_control)) act_vernac);
+ Pcoq.(Production.make (Rule.next Rule.stop (Symbol.token Tok.PEOI)) act_eoi);
+ Pcoq.(Production.make (Rule.next Rule.stop (Symbol.nterm vernac_control)) act_vernac);
] in
- Pcoq.(grammar_extend main_entry {G.pos=None; data=[None, None, rule]})
+ Pcoq.(grammar_extend main_entry {pos=None; data=[None, None, rule]})
let select_tactic_entry spec =
match spec with
@@ -65,8 +65,8 @@ module Vernac_ =
| Some ename -> find_proof_mode ename
let command_entry =
- Pcoq.G.Entry.of_parser "command_entry"
- (fun _ strm -> Pcoq.G.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm)
+ Pcoq.Entry.of_parser "command_entry"
+ (fun _ strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm)
end
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 4008c3d799..1920c276af 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -166,15 +166,15 @@ let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args -> vernac_c
| Some Refl -> untype_command ty (f v) args
end
-let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Gramlib.Grammar.norec, a) Pcoq.G.Symbol.t =
+let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Gramlib.Grammar.norec, a) Pcoq.Symbol.t =
let open Extend in function
- | TUlist1 l -> Pcoq.G.Symbol.list1 (untype_user_symbol l)
- | TUlist1sep (l, s) -> Pcoq.G.Symbol.list1sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false
- | TUlist0 l -> Pcoq.G.Symbol.list0 (untype_user_symbol l)
- | TUlist0sep (l, s) -> Pcoq.G.Symbol.list0sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false
- | TUopt o -> Pcoq.G.Symbol.opt (untype_user_symbol o)
- | TUentry a -> Pcoq.G.Symbol.nterm (Pcoq.genarg_grammar (Genarg.ExtraArg a))
- | TUentryl (a, i) -> Pcoq.G.Symbol.nterml (Pcoq.genarg_grammar (Genarg.ExtraArg a)) (string_of_int i)
+ | TUlist1 l -> Pcoq.Symbol.list1 (untype_user_symbol l)
+ | TUlist1sep (l, s) -> Pcoq.Symbol.list1sep (untype_user_symbol l) (Pcoq.Symbol.token (CLexer.terminal s)) false
+ | TUlist0 l -> Pcoq.Symbol.list0 (untype_user_symbol l)
+ | TUlist0sep (l, s) -> Pcoq.Symbol.list0sep (untype_user_symbol l) (Pcoq.Symbol.token (CLexer.terminal s)) false
+ | TUopt o -> Pcoq.Symbol.opt (untype_user_symbol o)
+ | TUentry a -> Pcoq.Symbol.nterm (Pcoq.genarg_grammar (Genarg.ExtraArg a))
+ | TUentryl (a, i) -> Pcoq.Symbol.nterml (Pcoq.genarg_grammar (Genarg.ExtraArg a)) (string_of_int i)
let rec untype_grammar : type r s. (r, s) ty_sig -> 'a Egramml.grammar_prod_item list = function
| TyNil -> []
@@ -193,7 +193,7 @@ let vernac_extend ~command ?classifier ?entry ext =
| None ->
let e = match entry with
| None -> "COMMAND"
- | Some e -> Pcoq.G.Entry.name e
+ | Some e -> Pcoq.Entry.name e
in
let msg = Printf.sprintf "\
Vernac entry \"%s\" misses a classifier. \
@@ -229,7 +229,7 @@ let vernac_extend ~command ?classifier ?entry ext =
type 'a argument_rule =
| Arg_alias of 'a Pcoq.Entry.t
-| Arg_rules of 'a Pcoq.G.Production.t list
+| Arg_rules of 'a Pcoq.Production.t list
type 'a vernac_argument = {
arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
@@ -244,7 +244,7 @@ let vernac_argument_extend ~name arg =
e
| Arg_rules rules ->
let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
- let () = Pcoq.grammar_extend e {Pcoq.G.pos=None; data=[(None, None, rules)]} in
+ let () = Pcoq.grammar_extend e {Pcoq.pos=None; data=[(None, None, rules)]} in
e
in
let pr = arg.arg_printer in
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 4d9537b6ff..0d0ebc1086 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -111,7 +111,7 @@ type 'a argument_rule =
| Arg_alias of 'a Pcoq.Entry.t
(** This is used because CAMLP5 parser can be dumb about rule factorization,
which sometimes requires two entries to be the same. *)
-| Arg_rules of 'a Pcoq.G.Production.t list
+| Arg_rules of 'a Pcoq.Production.t list
(** There is a discrepancy here as we use directly extension rules and thus
entries instead of ty_user_symbol and thus arguments as roots. *)
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 6b7b2c2691..15a19c06c2 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -183,12 +183,12 @@ and vernac_load ~verbosely fname =
let input =
let longfname = Loadpath.locate_file fname in
let in_chan = Util.open_utf8_file_in longfname in
- Pcoq.G.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in
+ Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in
(* Parsing loop *)
let v_mod = if verbosely then Flags.verbosely else Flags.silently in
let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing
(fun po ->
- match Pcoq.G.Entry.parse (Pvernac.main_entry proof_mode) po with
+ match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with
| Some x -> x
| None -> raise End_of_input) in
let rec load_loop ~stack =
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 49486b889d..6846826bfa 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -19,7 +19,7 @@ module Parser = struct
let parse ps entry pa =
Pcoq.unfreeze ps;
Flags.with_option Flags.we_are_parsing
- (fun () -> Pcoq.G.Entry.parse entry pa)
+ (fun () -> Pcoq.Entry.parse entry pa)
()
end
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index ed1b76b618..7607f8373a 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -14,7 +14,7 @@ module Parser : sig
val init : unit -> state
val cur_state : unit -> state
- val parse : state -> 'a Pcoq.Entry.t -> Pcoq.G.Parsable.t -> 'a
+ val parse : state -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:44:32 +0000