From e414c07e193db7d4256c09167f6efd545831fa2b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Fri, 15 Sep 2017 22:33:23 +0200
Subject: Register universe binders for record projections.

---
 vernac/record.mli | 24 ------------------------
 1 file changed, 24 deletions(-)

(limited to 'vernac/record.mli')

diff --git a/vernac/record.mli b/vernac/record.mli
index 33c2fba89..9fdd5e1c4 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -7,36 +7,12 @@
 (************************************************************************)
 
 open Names
-open Constr
 open Vernacexpr
 open Constrexpr
-open Impargs
 open Globnames
 
 val primitive_flag : bool ref
 
-(** [declare_projections ref name coers params fields] declare projections of
-   record [ref] (if allowed) using the given [name] as argument, and put them
-   as coercions accordingly to [coers]; it returns the absolute names of projections *)
-
-val declare_projections :
-  inductive -> ?kind:Decl_kinds.definition_object_kind -> Id.t ->
-  coercion_flag list -> manual_explicitation list list -> Context.Rel.t ->
-  (Name.t * bool) list * Constant.t option list
-
-val declare_structure :
-  Decl_kinds.recursivity_kind ->
-  Entries.inductive_universes ->
-  Id.t -> Id.t ->
-  manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
-  bool (** template arity ? *) ->
-  Impargs.manual_explicitation list list -> Context.Rel.t -> (** fields *)
-  ?kind:Decl_kinds.definition_object_kind -> ?name:Id.t ->
-  bool -> (** coercion? *)
-  bool list -> (** field coercions *)
-  Evd.evar_map ->
-  inductive
-
 val definition_structure :
   inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic *
   Decl_kinds.recursivity_kind * ident_decl with_coercion * local_binder_expr list *
-- 
cgit v1.2.3