diff options
Diffstat (limited to 'vernac/record.mli')
| -rw-r--r-- | vernac/record.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/vernac/record.mli b/vernac/record.mli index 992da2aa5..b2c039f0b 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -11,7 +11,6 @@ open Names open Vernacexpr open Constrexpr -open Globnames val primitive_flag : bool ref @@ -21,7 +20,7 @@ val declare_projections : ?kind:Decl_kinds.definition_object_kind -> Id.t -> bool list -> - Universes.universe_binders -> + UnivNames.universe_binders -> Impargs.manual_implicits list -> Context.Rel.t -> (Name.t * bool) list * Constant.t option list @@ -30,6 +29,6 @@ val definition_structure : inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * - Id.t * constr_expr option -> global_reference + Id.t * constr_expr option -> GlobRef.t -val declare_existing_class : global_reference -> unit +val declare_existing_class : GlobRef.t -> unit |