diff options
Diffstat (limited to 'interp/declare.mli')
| -rw-r--r-- | interp/declare.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/declare.mli b/interp/declare.mli index 084d746e6..f8cffbb1e 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -83,7 +83,7 @@ val recursive_message : bool (** true = fixpoint *) -> val exists_name : Id.t -> bool (** Global universe contexts, names and constraints *) -val declare_univ_binders : Globnames.global_reference -> Universes.universe_binders -> unit +val declare_univ_binders : GlobRef.t -> Universes.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit |