From d66fe71c93bc06f6006c64118deb1d5b01bf7487 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 17 Mar 2016 16:01:23 +0100
Subject: Adding a universe argument to Pcoq.create_generic_entry.

---
 parsing/pcoq.ml  | 2 +-
 parsing/pcoq.mli | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'parsing')

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
-- 
cgit v1.2.3