diff options
Diffstat (limited to 'vernac/record.mli')
| -rw-r--r-- | vernac/record.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/record.mli b/vernac/record.mli index 992da2aa5..308c9e9b9 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 @@ -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 |