From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 vernac/record.mli | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

(limited to 'vernac/record.mli')

diff --git a/vernac/record.mli b/vernac/record.mli
index 992da2aa..567f2b31 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,15 +20,20 @@ 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 ->
+  Constr.rel_context ->
     (Name.t * bool) list * Constant.t option list
 
 val definition_structure :
-  inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic *
-  Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list *
+  inductive_kind -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
+  Declarations.recursivity_kind ->
+  (coercion_flag *
+  Names.lident *
+  universe_decl_expr option *
+  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) list ->
+  GlobRef.t list
 
-val declare_existing_class : global_reference -> unit
+val declare_existing_class : GlobRef.t -> unit
-- 
cgit v1.2.3