diff options
| author | Pierre-Marie Pédrot | 2016-03-17 16:01:23 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-17 16:04:39 +0100 |
| commit | d66fe71c93bc06f6006c64118deb1d5b01bf7487 (patch) | |
| tree | 9b534252c1699be106a40daacc416f585dad74eb /parsing | |
| parent | e3e8a4065047e254f5f5c2747227db75f01b7bed (diff) | |
Adding a universe argument to Pcoq.create_generic_entry.
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 |