From 4f82fb034f81fa762cfc47bfb3194c5f93a342eb Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 24 Oct 2019 03:50:28 +0200
Subject: [declare] Split inductive declaration code to vernac/

The code is self-contained and only used by commands; this also
highlights the several `Libobject.obj` registered for each
declaration.
---
 vernac/declareInd.mli | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 vernac/declareInd.mli

(limited to 'vernac/declareInd.mli')

diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli
new file mode 100644
index 0000000000..6db09ad2bd
--- /dev/null
+++ b/vernac/declareInd.mli
@@ -0,0 +1,14 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** [declare_mind me] declares a block of inductive types with
+   their constructors in the current section; it returns the path of
+   the whole block and a boolean indicating if it is a primitive record. *)
+val declare_mind : Entries.mutual_inductive_entry -> Libobject.object_name * bool
-- 
cgit v1.2.3