From 06931bf4b193f978d43f30e22732b0122602ed53 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Wed, 14 Feb 2018 19:24:14 +0100
Subject: record: restore API declare_projections (removed in e414c07e1)

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

(limited to 'vernac/record.mli')

diff --git a/vernac/record.mli b/vernac/record.mli
index e632e7bbf..e0a4b8fdd 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -13,6 +13,17 @@ open Globnames
 
 val primitive_flag : bool ref
 
+val declare_projections :
+  inductive ->
+  Entries.constant_universes_entry ->
+  ?kind:Decl_kinds.definition_object_kind ->
+  Id.t ->
+  bool list ->
+  Universes.universe_binders ->
+  Impargs.manual_implicits list ->
+  Context.Rel.t ->
+    (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 *
-- 
cgit v1.2.3