diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pcoq.ml | 2 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 52437e3867..e150578196 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -251,7 +251,7 @@ let create_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.ent let create_constr_entry s = create_entry uconstr s (rawwit wit_constr) -let create_generic_entry s wit = create_entry utactic s wit +let create_generic_entry = create_entry (* [make_gen_entry] builds entries extensible by giving its name (a string) *) (* For entries extensible only via the ML name, Gram.entry_create is enough *) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 7e0c89fd12..625f0370e6 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -162,8 +162,8 @@ val uvernac : gram_universe val get_entry : gram_universe -> string -> typed_entry -val create_generic_entry : string -> ('a, rlevel) abstract_argument_type -> - 'a Gram.entry +val create_generic_entry : gram_universe -> string -> + ('a, rlevel) abstract_argument_type -> 'a Gram.entry module Prim : sig |