aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--dev/doc/changes.md5
-rw-r--r--ide/idetop.ml6
-rw-r--r--parsing/pcoq.ml97
-rw-r--r--parsing/pcoq.mli139
-rw-r--r--plugins/ltac/extraargs.mli16
-rw-r--r--plugins/ltac/g_ltac.ml44
-rw-r--r--plugins/ltac/pltac.ml9
-rw-r--r--plugins/ltac/pltac.mli38
-rw-r--r--plugins/ltac/tacentries.mli2
-rw-r--r--plugins/ssr/ssrparser.ml42
-rw-r--r--plugins/ssr/ssrparser.mli4
-rw-r--r--plugins/ssrmatching/g_ssrmatching.mli6
-rw-r--r--stm/stm.ml2
-rw-r--r--stm/stm.mli6
-rw-r--r--toplevel/coqloop.ml8
-rw-r--r--toplevel/coqloop.mli2
-rw-r--r--toplevel/g_toplevel.mlg6
-rw-r--r--toplevel/vernac.ml6
-rw-r--r--vernac/egramcoq.ml4
-rw-r--r--vernac/egramml.mli2
-rw-r--r--vernac/g_proofs.mlg2
-rw-r--r--vernac/g_vernac.mlg24
-rw-r--r--vernac/metasyntax.ml2
-rw-r--r--vernac/proof_using.ml2
-rw-r--r--vernac/pvernac.ml4
-rw-r--r--vernac/pvernac.mli26
-rw-r--r--vernac/vernacentries.ml4
27 files changed, 230 insertions, 198 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 6d5023405..1eea2443f 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -88,6 +88,11 @@ Primitive number parsers
have been split over three files (plugins/syntax/positive_syntax.ml,
plugins/syntax/n_syntax.ml, plugins/syntax/z_syntax.ml).
+Parsing
+
+- Manual uses of the Pcoq.Gram module have been deprecated. Wrapper modules
+ Pcoq.Entry and Pcoq.Parsable were introduced to replace it.
+
### Unit testing
The test suite now allows writing unit tests against OCaml code in the Coq
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 6fb004061..0c3328ee0 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -80,7 +80,7 @@ let set_doc doc = ide_doc := Some doc
let add ((s,eid),(sid,verbose)) =
let doc = get_doc () in
- let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+ let pa = Pcoq.Parsable.make (Stream.of_string s) in
let loc_ast = Stm.parse_sentence ~doc sid pa in
let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in
set_doc doc;
@@ -113,14 +113,14 @@ let edit_at id =
* be removed in the next version of the protocol.
*)
let query (route, (s,id)) =
- let pa = Pcoq.Gram.parsable (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 {CAst.loc;v=ast} =
- let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
+ let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa
in
(* XXX: Width should be a parameter of annotate... *)
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 93d65df2f..6726603e6 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -88,11 +88,10 @@ module type S =
type action = Gramext.g_action
type coq_parsable
- val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
+ val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
val action : 'a -> action
val entry_create : string -> 'a entry
val entry_parse : 'a entry -> coq_parsable -> 'a
- val entry_print : Format.formatter -> 'a entry -> unit
val comment_state : coq_parsable -> ((int * int) * string) list
@@ -107,7 +106,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
type coq_parsable = parsable * CLexer.lexer_state ref
- let parsable ?(file=Loc.ToplevelInput) c =
+ let coq_parsable ?(file=Loc.ToplevelInput) c =
let state = ref (CLexer.init_lexer_state file) in
CLexer.set_lexer_state !state;
let a = parsable c in
@@ -132,7 +131,23 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
let comment_state (p,state) =
CLexer.get_comment_state !state
- let entry_print ft x = Entry.print ft x
+end
+
+module Parsable =
+struct
+ type t = G.coq_parsable
+ let make = G.coq_parsable
+ let comment_state = G.comment_state
+end
+
+module Entry =
+struct
+
+ type 'a t = 'a Grammar.GMake(CLexer).Entry.e
+
+ let create = G.Entry.create
+ let parse = G.entry_parse
+ let print = G.Entry.print
end
@@ -347,14 +362,14 @@ let make_rule r = [None, None, r]
(** An entry that checks we reached the end of the input. *)
let eoi_entry en =
- let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in
+ let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in
let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in
let act = Gram.action (fun _ x loc -> x) in
uncurry (Gram.extend e) (None, make_rule [symbs, act]);
e
let map_entry f en =
- let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in
+ let e = Entry.create ((Gram.Entry.name en) ^ "_map") in
let symbs = [Symbols.snterm (Gram.Entry.obj en)] in
let act = Gram.action (fun x loc -> f x) in
uncurry (Gram.extend e) (None, make_rule [symbs, act]);
@@ -364,7 +379,7 @@ let map_entry f en =
(use eoi_entry) *)
let parse_string f x =
- let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm)
+ let strm = Stream.of_string x in Gram.entry_parse f (Gram.coq_parsable strm)
type gram_universe = string
@@ -385,14 +400,14 @@ let get_univ u =
let new_entry u s =
let ename = u ^ ":" ^ s in
- let e = Gram.entry_create ename in
+ let e = Entry.create ename in
e
let make_gen_entry u s = new_entry u s
module GrammarObj =
struct
- type ('r, _, _) obj = 'r Gram.entry
+ type ('r, _, _) obj = 'r Entry.t
let name = "grammar"
let default _ = None
end
@@ -402,7 +417,7 @@ module Grammar = Register(GrammarObj)
let register_grammar = Grammar.register0
let genarg_grammar = Grammar.obj
-let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry =
+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
@@ -414,38 +429,38 @@ module Prim =
struct
let gec_gen n = make_gen_entry uprim n
- (* Entries that can be referred via the string -> Gram.entry table *)
+ (* Entries that can be referred via the string -> Entry.t table *)
(* Typically for tactic or vernac extensions *)
let preident = gec_gen "preident"
let ident = gec_gen "ident"
let natural = gec_gen "natural"
let integer = gec_gen "integer"
- let bigint = Gram.entry_create "Prim.bigint"
+ let bigint = Entry.create "Prim.bigint"
let string = gec_gen "string"
- let lstring = Gram.entry_create "Prim.lstring"
+ let lstring = Entry.create "Prim.lstring"
let reference = make_gen_entry uprim "reference"
- let by_notation = Gram.entry_create "by_notation"
- let smart_global = Gram.entry_create "smart_global"
+ let by_notation = Entry.create "by_notation"
+ let smart_global = Entry.create "smart_global"
(* parsed like ident but interpreted as a term *)
let var = gec_gen "var"
- let name = Gram.entry_create "Prim.name"
- let identref = Gram.entry_create "Prim.identref"
- let univ_decl = Gram.entry_create "Prim.univ_decl"
- let ident_decl = Gram.entry_create "Prim.ident_decl"
- let pattern_ident = Gram.entry_create "pattern_ident"
- let pattern_identref = Gram.entry_create "pattern_identref"
+ let name = Entry.create "Prim.name"
+ let identref = Entry.create "Prim.identref"
+ let univ_decl = Entry.create "Prim.univ_decl"
+ let ident_decl = Entry.create "Prim.ident_decl"
+ let pattern_ident = Entry.create "pattern_ident"
+ let pattern_identref = Entry.create "pattern_identref"
(* A synonym of ident - maybe ident will be located one day *)
- let base_ident = Gram.entry_create "Prim.base_ident"
+ let base_ident = Entry.create "Prim.base_ident"
- let qualid = Gram.entry_create "Prim.qualid"
- let fullyqualid = Gram.entry_create "Prim.fullyqualid"
- let dirpath = Gram.entry_create "Prim.dirpath"
+ let qualid = Entry.create "Prim.qualid"
+ let fullyqualid = Entry.create "Prim.fullyqualid"
+ let dirpath = Entry.create "Prim.dirpath"
- let ne_string = Gram.entry_create "Prim.ne_string"
- let ne_lstring = Gram.entry_create "Prim.ne_lstring"
+ let ne_string = Entry.create "Prim.ne_string"
+ let ne_lstring = Entry.create "Prim.ne_lstring"
end
@@ -453,7 +468,7 @@ module Constr =
struct
let gec_constr = make_gen_entry uconstr
- (* Entries that can be referred via the string -> Gram.entry table *)
+ (* Entries that can be referred via the string -> Entry.t table *)
let constr = gec_constr "constr"
let operconstr = gec_constr "operconstr"
let constr_eoi = eoi_entry constr
@@ -464,29 +479,29 @@ module Constr =
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"
- let pattern = Gram.entry_create "constr:pattern"
+ let pattern = Entry.create "constr:pattern"
let constr_pattern = gec_constr "constr_pattern"
let lconstr_pattern = gec_constr "lconstr_pattern"
- let closed_binder = Gram.entry_create "constr:closed_binder"
- let binder = Gram.entry_create "constr:binder"
- let binders = Gram.entry_create "constr:binders"
- let open_binders = Gram.entry_create "constr:open_binders"
- let binders_fixannot = Gram.entry_create "constr:binders_fixannot"
- let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint"
- let record_declaration = Gram.entry_create "constr:record_declaration"
- let appl_arg = Gram.entry_create "constr:appl_arg"
+ let closed_binder = Entry.create "constr:closed_binder"
+ let binder = Entry.create "constr:binder"
+ let binders = Entry.create "constr:binders"
+ let open_binders = Entry.create "constr:open_binders"
+ let binders_fixannot = Entry.create "constr:binders_fixannot"
+ let typeclass_constraint = Entry.create "constr:typeclass_constraint"
+ let record_declaration = Entry.create "constr:record_declaration"
+ let appl_arg = Entry.create "constr:appl_arg"
end
module Module =
struct
- let module_expr = Gram.entry_create "module_expr"
- let module_type = Gram.entry_create "module_type"
+ let module_expr = Entry.create "module_expr"
+ let module_type = Entry.create "module_type"
end
let epsilon_value f e =
let r = Rule (Next (Stop, e), fun x _ -> f x) in
let ext = of_coq_extend_statement (None, [None, None, [r]]) in
- let entry = G.entry_create "epsilon" in
+ let entry = Gram.entry_create "epsilon" in
let () = uncurry (G.extend entry) ext in
try Some (parse_string entry "") with _ -> None
@@ -591,7 +606,7 @@ let () =
(** Registering extra grammar *)
-type any_entry = AnyEntry : 'a Gram.entry -> 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 ae4f5cab6..029c43713 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -24,21 +24,34 @@ module Gram : sig
include Grammar.S with type te = Tok.t
type 'a entry = 'a Entry.e
+ [@@ocaml.deprecated "Use [Pcoq.Entry.t]"]
- type coq_parsable
+ [@@@ocaml.warning "-3"]
- val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
val entry_create : string -> 'a entry
- val entry_parse : 'a entry -> coq_parsable -> 'a
- val entry_print : Format.formatter -> 'a entry -> unit
-
- (* Get comment parsing information from the Lexer *)
- val comment_state : coq_parsable -> ((int * int) * string) list
+ [@@ocaml.deprecated "Use [Pcoq.Entry.create]"]
val gram_extend : 'a entry -> 'a Extend.extend_statement -> unit
+ [@@@ocaml.warning "+3"]
+
end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
+module Parsable :
+sig
+ type t
+ val make : ?file:Loc.source -> char Stream.t -> t
+ (* Get comment parsing information from the Lexer *)
+ val comment_state : t -> ((int * int) * string) list
+end
+
+module Entry : sig
+ type 'a t = 'a Grammar.GMake(CLexer).Entry.e
+ val create : string -> 'a t
+ val parse : 'a t -> Parsable.t -> 'a
+ val print : Format.formatter -> 'a t -> unit
+end
+
(** The parser of Coq is built from three kinds of rule declarations:
- dynamic rules declared at the evaluation of Coq files (using
@@ -120,86 +133,86 @@ val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit
(** Parse a string *)
-val parse_string : 'a Gram.entry -> string -> 'a
-val eoi_entry : 'a Gram.entry -> 'a Gram.entry
-val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry
+val parse_string : 'a Entry.t -> string -> 'a
+val eoi_entry : 'a Entry.t -> 'a Entry.t
+val map_entry : ('a -> 'b) -> 'a Entry.t -> 'b Entry.t
type gram_universe
val get_univ : string -> gram_universe
val create_universe : string -> gram_universe
-val new_entry : gram_universe -> string -> 'a Gram.entry
+val new_entry : gram_universe -> string -> 'a Entry.t
val uprim : gram_universe
val uconstr : gram_universe
val utactic : gram_universe
-val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit
-val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry
+val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t -> unit
+val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t
val create_generic_entry : gram_universe -> string ->
- ('a, rlevel) abstract_argument_type -> 'a Gram.entry
+ ('a, rlevel) abstract_argument_type -> 'a Entry.t
module Prim :
sig
open Names
open Libnames
- val preident : string Gram.entry
- val ident : Id.t Gram.entry
- val name : lname Gram.entry
- val identref : lident Gram.entry
- val univ_decl : universe_decl_expr Gram.entry
- val ident_decl : ident_decl Gram.entry
- val pattern_ident : Id.t Gram.entry
- val pattern_identref : lident Gram.entry
- val base_ident : Id.t Gram.entry
- val natural : int Gram.entry
- val bigint : Constrexpr.raw_natural_number Gram.entry
- val integer : int Gram.entry
- val string : string Gram.entry
- val lstring : lstring Gram.entry
- val reference : qualid Gram.entry
- val qualid : qualid Gram.entry
- val fullyqualid : Id.t list CAst.t Gram.entry
- val by_notation : (string * string option) Gram.entry
- val smart_global : qualid or_by_notation Gram.entry
- val dirpath : DirPath.t Gram.entry
- val ne_string : string Gram.entry
- val ne_lstring : lstring Gram.entry
- val var : lident Gram.entry
+ val preident : string Entry.t
+ val ident : Id.t Entry.t
+ val name : lname Entry.t
+ val identref : lident Entry.t
+ val univ_decl : universe_decl_expr Entry.t
+ val ident_decl : ident_decl Entry.t
+ val pattern_ident : Id.t Entry.t
+ val pattern_identref : lident Entry.t
+ val base_ident : Id.t Entry.t
+ val natural : int Entry.t
+ val bigint : Constrexpr.raw_natural_number Entry.t
+ val integer : int Entry.t
+ val string : string Entry.t
+ val lstring : lstring Entry.t
+ val reference : qualid Entry.t
+ val qualid : qualid Entry.t
+ val fullyqualid : Id.t list CAst.t Entry.t
+ val by_notation : (string * string option) Entry.t
+ val smart_global : qualid or_by_notation Entry.t
+ val dirpath : DirPath.t Entry.t
+ val ne_string : string Entry.t
+ val ne_lstring : lstring Entry.t
+ val var : lident Entry.t
end
module Constr :
sig
- val constr : constr_expr Gram.entry
- val constr_eoi : constr_expr Gram.entry
- val lconstr : constr_expr Gram.entry
- val binder_constr : constr_expr Gram.entry
- val operconstr : constr_expr Gram.entry
- val ident : Id.t Gram.entry
- val global : qualid Gram.entry
- val universe_level : Glob_term.glob_level Gram.entry
- val sort : Glob_term.glob_sort Gram.entry
- val sort_family : Sorts.family Gram.entry
- val pattern : cases_pattern_expr Gram.entry
- val constr_pattern : constr_expr Gram.entry
- val lconstr_pattern : constr_expr Gram.entry
- val closed_binder : local_binder_expr list Gram.entry
- val binder : local_binder_expr list Gram.entry (* closed_binder or variable *)
- val binders : local_binder_expr list Gram.entry (* list of binder *)
- val open_binders : local_binder_expr list Gram.entry
- val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Gram.entry
- val typeclass_constraint : (lname * bool * constr_expr) Gram.entry
- val record_declaration : constr_expr Gram.entry
- val appl_arg : (constr_expr * explicitation CAst.t option) Gram.entry
+ val constr : constr_expr Entry.t
+ val constr_eoi : constr_expr Entry.t
+ val lconstr : constr_expr Entry.t
+ val binder_constr : constr_expr Entry.t
+ val operconstr : constr_expr Entry.t
+ val ident : Id.t Entry.t
+ val global : qualid 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
+ val pattern : cases_pattern_expr Entry.t
+ val constr_pattern : constr_expr Entry.t
+ val lconstr_pattern : constr_expr Entry.t
+ val closed_binder : local_binder_expr list Entry.t
+ val binder : local_binder_expr list Entry.t (* closed_binder or variable *)
+ val binders : local_binder_expr list Entry.t (* list of binder *)
+ val open_binders : local_binder_expr list Entry.t
+ val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Entry.t
+ val typeclass_constraint : (lname * bool * constr_expr) Entry.t
+ val record_declaration : constr_expr Entry.t
+ val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t
end
module Module :
sig
- val module_expr : module_ast Gram.entry
- val module_type : module_ast Gram.entry
+ val module_expr : module_ast Entry.t
+ val module_type : module_ast Entry.t
end
val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
@@ -209,7 +222,7 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
type gram_reinit = gram_assoc * gram_position
(** Type of reinitialization data *)
-val grammar_extend : 'a Gram.entry -> gram_reinit option ->
+val grammar_extend : 'a Entry.t -> gram_reinit option ->
'a Extend.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
@@ -225,7 +238,7 @@ type 'a grammar_command
marshallable. *)
type extend_rule =
-| ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statement -> extend_rule
+| ExtendRule : 'a Entry.t * gram_reinit option * '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,
@@ -255,7 +268,7 @@ val parser_summary_tag : frozen_t Summary.Dyn.tag
(** Registering grammars by name *)
-type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+type any_entry = AnyEntry : 'a Entry.t -> any_entry
val register_grammars_by_name : string -> any_entry list -> unit
val find_grammars_by_name : string -> any_entry list
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 737147884..e477b12cd 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -14,12 +14,12 @@ open Constrexpr
open Glob_term
val wit_orient : bool Genarg.uniform_genarg_type
-val orient : bool Pcoq.Gram.entry
+val orient : bool Pcoq.Entry.t
val pr_orient : bool -> Pp.t
val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type
-val occurrences : (int list Locus.or_var) Pcoq.Gram.entry
+val occurrences : (int list Locus.or_var) Pcoq.Entry.t
val wit_occurrences : (int list Locus.or_var, int list Locus.or_var, int list) Genarg.genarg_type
val pr_occurrences : int list Locus.or_var -> Pp.t
val occurrences_of : int list -> Locus.occurrences
@@ -46,8 +46,8 @@ val wit_casted_constr :
Tacexpr.glob_constr_and_expr,
EConstr.t) Genarg.genarg_type
-val glob : constr_expr Pcoq.Gram.entry
-val lglob : constr_expr Pcoq.Gram.entry
+val glob : constr_expr Pcoq.Entry.t
+val lglob : constr_expr Pcoq.Entry.t
type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
@@ -55,10 +55,10 @@ type loc_place = lident gen_place
type place = Id.t gen_place
val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type
-val hloc : loc_place Pcoq.Gram.entry
+val hloc : loc_place Pcoq.Entry.t
val pr_hloc : loc_place -> Pp.t
-val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
+val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Entry.t
val wit_by_arg_tac :
(raw_tactic_expr option,
glob_tactic_expr option,
@@ -68,13 +68,13 @@ val pr_by_arg_tac :
(int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) ->
raw_tactic_expr option -> Pp.t
-val test_lpar_id_colon : unit Pcoq.Gram.entry
+val test_lpar_id_colon : unit Pcoq.Entry.t
val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
(** Spiwack: Primitive for retroknowledge registration *)
-val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
+val retroknowledge_field : Retroknowledge.field Pcoq.Entry.t
val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type
val wit_in_clause :
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 620f14707..9d86f21d4 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -46,10 +46,10 @@ let reference_to_id qid =
CErrors.user_err ?loc:qid.CAst.loc
(str "This expression should be a simple identifier.")
-let tactic_mode = Gram.entry_create "vernac:tactic_command"
+let tactic_mode = Entry.create "vernac:tactic_command"
let new_entry name =
- let e = Gram.entry_create name in
+ let e = Entry.create name in
e
let toplevel_selector = new_entry "vernac:toplevel_selector"
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index e9711268c..759bb62fd 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -11,11 +11,10 @@
open Pcoq
(* Main entry for extensions *)
-let simple_tactic = Gram.entry_create "tactic:simple_tactic"
+let simple_tactic = Entry.create "tactic:simple_tactic"
-let make_gen_entry _ name = Gram.entry_create ("tactic:" ^ name)
+let make_gen_entry _ name = Entry.create ("tactic:" ^ name)
-(* Entries that can be referred via the string -> Gram.entry table *)
(* Typically for tactic user extensions *)
let open_constr =
make_gen_entry utactic "open_constr"
@@ -23,7 +22,7 @@ let constr_with_bindings =
make_gen_entry utactic "constr_with_bindings"
let bindings =
make_gen_entry utactic "bindings"
-let hypident = Gram.entry_create "hypident"
+let hypident = Entry.create "hypident"
let constr_may_eval = make_gen_entry utactic "constr_may_eval"
let constr_eval = make_gen_entry utactic "constr_eval"
let uconstr =
@@ -40,7 +39,7 @@ let clause_dft_concl =
(* Main entries for ltac *)
-let tactic_arg = Gram.entry_create "tactic:tactic_arg"
+let tactic_arg = Entry.create "tactic:tactic_arg"
let tactic_expr = make_gen_entry utactic "tactic_expr"
let binder_tactic = make_gen_entry utactic "binder_tactic"
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index c5aa542fd..9bff98b6c 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -17,22 +17,22 @@ open Tacexpr
open Genredexpr
open Tactypes
-val open_constr : constr_expr Gram.entry
-val constr_with_bindings : constr_expr with_bindings Gram.entry
-val bindings : constr_expr bindings Gram.entry
-val hypident : (Names.lident * Locus.hyp_location_flag) Gram.entry
-val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry
-val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry
-val uconstr : constr_expr Gram.entry
-val quantified_hypothesis : quantified_hypothesis Gram.entry
-val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry
-val int_or_var : int Locus.or_var Gram.entry
-val simple_tactic : raw_tactic_expr Gram.entry
-val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry
-val in_clause : Names.lident Locus.clause_expr Gram.entry
-val clause_dft_concl : Names.lident Locus.clause_expr Gram.entry
-val tactic_arg : raw_tactic_arg Gram.entry
-val tactic_expr : raw_tactic_expr Gram.entry
-val binder_tactic : raw_tactic_expr Gram.entry
-val tactic : raw_tactic_expr Gram.entry
-val tactic_eoi : raw_tactic_expr Gram.entry
+val open_constr : constr_expr Entry.t
+val constr_with_bindings : constr_expr with_bindings Entry.t
+val bindings : constr_expr bindings Entry.t
+val hypident : (Names.lident * Locus.hyp_location_flag) Entry.t
+val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Entry.t
+val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Entry.t
+val uconstr : constr_expr Entry.t
+val quantified_hypothesis : quantified_hypothesis Entry.t
+val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Entry.t
+val int_or_var : int Locus.or_var Entry.t
+val simple_tactic : raw_tactic_expr Entry.t
+val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t
+val in_clause : Names.lident Locus.clause_expr Entry.t
+val clause_dft_concl : Names.lident Locus.clause_expr Entry.t
+val tactic_arg : raw_tactic_arg Entry.t
+val tactic_expr : raw_tactic_expr Entry.t
+val binder_tactic : raw_tactic_expr Entry.t
+val tactic : raw_tactic_expr Entry.t
+val tactic_eoi : raw_tactic_expr Entry.t
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 9bba9ba71..f873631ff 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -55,7 +55,7 @@ val add_ml_tactic_notation : ml_tactic_name -> level:int ->
(** {5 Tactic Quotations} *)
val create_ltac_quotation : string ->
- ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Gram.entry * int option) -> unit
+ ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Entry.t * int option) -> unit
(** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is,
Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and
generates an argument using [f] on the entry parsed by [e]. *)
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 6b183dab1..8b9c94f2d 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1408,7 +1408,7 @@ let check_seqtacarg dir arg = match snd arg, dir with
CErrors.user_err ?loc (str "expected \"first\"")
| _, _ -> arg
-let ssrorelse = Gram.entry_create "ssrorelse"
+let ssrorelse = Entry.create "ssrorelse"
GEXTEND Gram
GLOBAL: ssrorelse ssrseqarg;
ssrseqidx: [
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 7cd3751ce..862a93765 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -12,11 +12,11 @@
open Ltac_plugin
-val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
+val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t
val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
val pr_ssrtacarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c
-val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
+val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t
val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
val pr_ssrtclarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd
diff --git a/plugins/ssrmatching/g_ssrmatching.mli b/plugins/ssrmatching/g_ssrmatching.mli
index bb5161a0e..588a1a3ea 100644
--- a/plugins/ssrmatching/g_ssrmatching.mli
+++ b/plugins/ssrmatching/g_ssrmatching.mli
@@ -5,13 +5,13 @@ open Genarg
open Ssrmatching
(** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *)
-val cpattern : cpattern Pcoq.Gram.entry
+val cpattern : cpattern Pcoq.Entry.t
val wit_cpattern : cpattern uniform_genarg_type
(** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *)
-val lcpattern : cpattern Pcoq.Gram.entry
+val lcpattern : cpattern Pcoq.Entry.t
val wit_lcpattern : cpattern uniform_genarg_type
(** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *)
-val rpattern : rpattern Pcoq.Gram.entry
+val rpattern : rpattern Pcoq.Entry.t
val wit_rpattern : rpattern uniform_genarg_type
diff --git a/stm/stm.ml b/stm/stm.ml
index 0aed88a53..e15b6048b 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2976,7 +2976,7 @@ let parse_sentence ~doc sid pa =
str "All is good if not parsing changes occur between the two states, however if they do, a problem might occur.");
Flags.with_option Flags.we_are_parsing (fun () ->
try
- match Pcoq.Gram.entry_parse Pvernac.main_entry pa with
+ match Pcoq.Entry.parse Pvernac.main_entry pa with
| None -> raise End_of_input
| Some (loc, cmd) -> CAst.make ~loc cmd
with e when CErrors.noncritical e ->
diff --git a/stm/stm.mli b/stm/stm.mli
index aed7274d0..50e7f0609 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -92,11 +92,11 @@ val new_doc : stm_init_options -> doc * Stateid.t
(** [parse_sentence sid pa] Reads a sentence from [pa] with parsing
state [sid] Returns [End_of_input] if the stream ends *)
-val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable ->
+val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Parsable.t ->
Vernacexpr.vernac_control CAst.t
(* Reminder: A parsable [pa] is constructed using
- [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *)
+ [Pcoq.Parsable.t stream], where [stream : char Stream.t]. *)
exception End_of_input
@@ -114,7 +114,7 @@ val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t ->
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.Gram.coq_parsable -> 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 d7ede1c2e..7ae15ac10 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.Gram.coq_parsable; (* 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.Gram.parsable (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. *)
@@ -228,7 +228,7 @@ let top_buffer =
str = Bytes.empty;
len = 0;
bols = [];
- tokens = Pcoq.Gram.parsable (Stream.of_list []);
+ tokens = Pcoq.Parsable.make (Stream.of_list []);
start = 0 }
let set_prompt prompt =
@@ -253,7 +253,7 @@ let parse_to_dot =
let rec discard_to_dot () =
try
- Pcoq.Gram.entry_parse parse_to_dot top_buffer.tokens
+ Pcoq.Entry.parse parse_to_dot top_buffer.tokens
with
| Token.Error _ | CLexer.Error.E _ -> discard_to_dot ()
| Stm.End_of_input -> raise Stm.End_of_input
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 5c07a8bf3..b11f13d3c 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 begining of lines *)
- mutable tokens : Pcoq.Gram.coq_parsable; (** 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/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index 53d3eef23..5aba3d6b0 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -21,9 +21,9 @@ type vernac_toplevel =
| VernacControl of vernac_control
module Toplevel_ : sig
- val vernac_toplevel : vernac_toplevel CAst.t Gram.entry
+ val vernac_toplevel : vernac_toplevel CAst.t Entry.t
end = struct
- let gec_vernac s = Gram.entry_create ("toplevel:" ^ s)
+ let gec_vernac s = Entry.create ("toplevel:" ^ s)
let vernac_toplevel = gec_vernac "vernac_toplevel"
end
@@ -49,6 +49,6 @@ END
{
-let parse_toplevel pa = Pcoq.Gram.entry_parse vernac_toplevel pa
+let parse_toplevel pa = Pcoq.Entry.parse vernac_toplevel pa
}
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index c1bbb20d5..c914bbecf 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -121,7 +121,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
let in_echo = if echo then Some (open_utf8_file_in file) else None in
let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in
- let in_pa = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
+ let in_pa = Pcoq.Parsable.make ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
let rstate = ref state in
(* For beautify, list of parsed sids *)
let rids = ref [] in
@@ -159,12 +159,12 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
rstate := state;
done;
input_cleanup ();
- !rstate, !rids, Pcoq.Gram.comment_state in_pa
+ !rstate, !rids, Pcoq.Parsable.comment_state in_pa
with any -> (* whatever the exception *)
let (e, info) = CErrors.push any in
input_cleanup ();
match e with
- | Stm.End_of_input -> !rstate, !rids, Pcoq.Gram.comment_state in_pa
+ | Stm.End_of_input -> !rstate, !rids, Pcoq.Parsable.comment_state in_pa
| reraise -> iraise (e, info)
let process_expr ~state loc_ast =
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 48f225f97..3281b75aa 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -240,14 +240,14 @@ type (_, _) entry =
type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
(* This computes the name of the level where to add a new rule *)
-let interp_constr_entry_key : type r. r target -> int -> r Gram.entry * int option =
+let interp_constr_entry_key : type r. r target -> int -> r Entry.t * int option =
fun forpat level -> match forpat with
| ForConstr ->
if level = 200 then Constr.binder_constr, None
else Constr.operconstr, Some level
| ForPattern -> Constr.pattern, Some level
-let target_entry : type s. s target -> s Gram.entry = function
+let target_entry : type s. s target -> s Entry.t = function
| ForConstr -> Constr.operconstr
| ForPattern -> Constr.pattern
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index 31aa1a989..a5ee036db 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -21,7 +21,7 @@ type 's grammar_prod_item =
('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
val extend_vernac_command_grammar :
- Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option ->
+ Vernacexpr.extend_name -> vernac_expr Pcoq.Entry.t option ->
vernac_expr grammar_prod_item list -> unit
val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index cccdbfc91..dacef6e21 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -22,7 +22,7 @@ open Pvernac.Vernac_
let thm_token = G_vernac.thm_token
-let hint = Gram.entry_create "hint"
+let hint = Entry.create "hint"
let warn_deprecated_focus =
CWarnings.create ~name:"deprecated-focus" ~category:"deprecated"
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3a01ce6df..2c60abfe3 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -37,18 +37,18 @@ let _ = List.iter CLexer.add_keyword vernac_kw
(* Rem: do not join the different GEXTEND into one, it breaks native *)
(* compilation on PowerPC and Sun architectures *)
-let query_command = Gram.entry_create "vernac:query_command"
-
-let subprf = Gram.entry_create "vernac:subprf"
-
-let class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
-let thm_token = Gram.entry_create "vernac:thm_token"
-let def_body = Gram.entry_create "vernac:def_body"
-let decl_notation = Gram.entry_create "vernac:decl_notation"
-let record_field = Gram.entry_create "vernac:record_field"
-let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion"
-let instance_name = Gram.entry_create "vernac:instance_name"
-let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
+let query_command = Entry.create "vernac:query_command"
+
+let subprf = Entry.create "vernac:subprf"
+
+let class_rawexpr = Entry.create "vernac:class_rawexpr"
+let thm_token = Entry.create "vernac:thm_token"
+let def_body = Entry.create "vernac:def_body"
+let decl_notation = Entry.create "vernac:decl_notation"
+let record_field = Entry.create "vernac:record_field"
+let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion"
+let instance_name = Entry.create "vernac:instance_name"
+let section_subset_expr = Entry.create "vernac:section_subset_expr"
let make_bullet s =
let open Proof_bullet in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 240147c8d..33e6229b2 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -49,7 +49,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.Gram.entry_print ft e in
+ let () = Pcoq.Entry.print ft e in
str (Buffer.contents entry_buf)
let pr_registered_grammar name =
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index f8b085f3e..74e53bef1 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -178,7 +178,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.Gram.(entry_parse G_vernac.section_subset_expr (parsable (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 _ =
Goptions.declare_stringopt_option
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index aea66a07a..b2fa8ec99 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -14,7 +14,7 @@ let uvernac = create_universe "vernac"
module Vernac_ =
struct
- let gec_vernac s = Gram.entry_create ("vernac:" ^ s)
+ let gec_vernac s = Entry.create ("vernac:" ^ s)
(* The different kinds of vernacular commands *)
let gallina = gec_vernac "gallina"
@@ -26,7 +26,7 @@ module Vernac_ =
let red_expr = new_entry utactic "red_expr"
let hint_info = gec_vernac "hint_info"
(* Main vernac entry *)
- let main_entry = Gram.entry_create "vernac"
+ let main_entry = Entry.create "vernac"
let noedit_mode = gec_vernac "noedit_command"
let () =
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 2993a1661..b2f8f7146 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -16,21 +16,21 @@ val uvernac : gram_universe
module Vernac_ :
sig
- val gallina : vernac_expr Gram.entry
- val gallina_ext : vernac_expr Gram.entry
- val command : vernac_expr Gram.entry
- val syntax : vernac_expr Gram.entry
- val vernac_control : vernac_control Gram.entry
- val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
- val noedit_mode : vernac_expr Gram.entry
- val command_entry : vernac_expr Gram.entry
- val red_expr : raw_red_expr Gram.entry
- val hint_info : Hints.hint_info_expr Gram.entry
+ val gallina : vernac_expr Entry.t
+ val gallina_ext : vernac_expr Entry.t
+ val command : vernac_expr Entry.t
+ val syntax : vernac_expr Entry.t
+ val vernac_control : vernac_control Entry.t
+ val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
+ val noedit_mode : vernac_expr Entry.t
+ val command_entry : vernac_expr Entry.t
+ val red_expr : raw_red_expr Entry.t
+ val hint_info : Hints.hint_info_expr Entry.t
end
(** The main entry: reads an optional vernac command *)
-val main_entry : (Loc.t * vernac_control) option Gram.entry
+val main_entry : (Loc.t * vernac_control) option Entry.t
(** Handling of the proof mode entry *)
-val get_command_entry : unit -> vernac_expr Gram.entry
-val set_command_entry : vernac_expr Gram.entry -> unit
+val get_command_entry : unit -> vernac_expr Entry.t
+val set_command_entry : vernac_expr Entry.t -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5fda1a0da..8064856a6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2040,7 +2040,7 @@ let vernac_load interp fname =
interp x in
let parse_sentence = Flags.with_option Flags.we_are_parsing
(fun po ->
- match Pcoq.Gram.entry_parse Pvernac.main_entry po with
+ match Pcoq.Entry.parse Pvernac.main_entry po with
| Some x -> x
| None -> raise End_of_input) in
let fname =
@@ -2049,7 +2049,7 @@ let vernac_load interp fname =
let input =
let longfname = Loadpath.locate_file fname in
let in_chan = open_utf8_file_in longfname in
- Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
+ Pcoq.Parsable.make ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
begin
try while true do interp (snd (parse_sentence input)) done
with End_of_input -> ()