From ff07d0f499dcc8876b2b222bf861e9de89315a05 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 5 Apr 2019 11:00:43 +0200
Subject: Remove calls to Global.env and Libobject from Recordops

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

(limited to 'vernac/record.mli')

diff --git a/vernac/record.mli b/vernac/record.mli
index 9852840d12..12a2a765b5 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -24,6 +24,8 @@ val declare_projections :
   Constr.rel_context ->
     (Name.t * bool) list * Constant.t option list
 
+val declare_structure_entry : Recordops.struc_tuple -> unit
+
 val definition_structure :
   universe_decl_expr option -> inductive_kind -> template:bool option ->
   Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
-- 
cgit v1.2.3