From 211b547f231d074e23c1c12655c3aa3fec8054e3 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 23 Oct 2012 21:23:58 +0000
Subject: Cleared a purely declarative .ml file and moved its interface to
 intf/

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15928 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/printers.mllib  |  1 -
 intf/entries.mli    | 83 +++++++++++++++++++++++++++++++++++++++++++++++++++
 kernel/entries.ml   | 86 -----------------------------------------------------
 kernel/entries.mli  | 83 ---------------------------------------------------
 kernel/kernel.mllib |  1 -
 5 files changed, 83 insertions(+), 171 deletions(-)
 create mode 100644 intf/entries.mli
 delete mode 100644 kernel/entries.ml
 delete mode 100644 kernel/entries.mli

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 8e72580629..6f34dbb094 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -51,7 +51,6 @@ Conv_oracle
 Closure
 Reduction
 Type_errors
-Entries
 Modops
 Inductive
 Typeops
diff --git a/intf/entries.mli b/intf/entries.mli
new file mode 100644
index 0000000000..2460ec6445
--- /dev/null
+++ b/intf/entries.mli
@@ -0,0 +1,83 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Univ
+open Term
+open Sign
+
+(** This module defines the entry types for global declarations. This
+   information is entered in the environments. This includes global
+   constants/axioms, mutual inductive definitions, modules and module
+   types *)
+
+
+(** {6 Local entries } *)
+
+type local_entry =
+  | LocalDef of constr
+  | LocalAssum of constr
+
+
+(** {6 Declaration of inductive types. } *)
+
+(** Assume the following definition in concrete syntax:
+{v Inductive I1 (x1:X1) ... (xn:Xn) : A1 := c11 : T11 | ... | c1n1 : T1n1
+...
+with      Ip (x1:X1) ... (xn:Xn) : Ap := cp1 : Tp1 | ... | cpnp : Tpnp. v}
+
+then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
+[mind_entry_arity] is [Ai], defined in context [x1:X1;...;xn:Xn];
+[mind_entry_lc] is [Ti1;...;Tini], defined in context [[A'1;...;A'p;x1:X1;...;xn:Xn]] where [A'i] is [Ai] generalized over [[x1:X1;...;xn:Xn]].
+*)
+
+type one_inductive_entry = {
+  mind_entry_typename : identifier;
+  mind_entry_arity : constr;
+  mind_entry_consnames : identifier list;
+  mind_entry_lc : constr list }
+
+type mutual_inductive_entry = {
+  mind_entry_record : bool;
+  mind_entry_finite : bool;
+  mind_entry_params : (identifier * local_entry) list;
+  mind_entry_inds : one_inductive_entry list }
+
+(** {6 Constants (Definition/Axiom) } *)
+
+type definition_entry = {
+  const_entry_body   : constr;
+  const_entry_secctx : section_context option;
+  const_entry_type   : types option;
+  const_entry_opaque : bool }
+
+type inline = int option (* inlining level, None for no inlining *)
+
+type parameter_entry = section_context option * types * inline 
+
+type constant_entry =
+  | DefinitionEntry of definition_entry
+  | ParameterEntry of parameter_entry
+
+(** {6 Modules } *)
+
+type module_struct_entry =
+    MSEident of module_path
+  | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry
+  | MSEwith of module_struct_entry * with_declaration
+  | MSEapply of module_struct_entry * module_struct_entry
+
+and with_declaration =
+    With_Module of identifier list * module_path
+  | With_Definition of identifier list * constr
+
+and module_entry =
+    { mod_entry_type : module_struct_entry option;
+      mod_entry_expr : module_struct_entry option}
+
+
diff --git a/kernel/entries.ml b/kernel/entries.ml
deleted file mode 100644
index 2da2c78994..0000000000
--- a/kernel/entries.ml
+++ /dev/null
@@ -1,86 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i*)
-open Names
-open Term
-open Sign
-(*i*)
-
-(* This module defines the entry types for global declarations. This
-   information is entered in the environments. This includes global
-   constants/axioms, mutual inductive definitions, modules and module
-   types *)
-
-
-(*s Local entries *)
-
-type local_entry =
-  | LocalDef of constr
-  | LocalAssum of constr
-
-
-(*s Declaration of inductive types. *)
-
-(* Assume the following definition in concrete syntax:
-\begin{verbatim}
-Inductive I1 (x1:X1) ... (xn:Xn) : A1 := c11 : T11 | ... | c1n1 : T1n1
-...
-with      Ip (x1:X1) ... (xn:Xn) : Ap := cp1 : Tp1 | ... | cpnp : Tpnp.
-\end{verbatim}
-then, in $i^{th}$ block, [mind_entry_params] is [[xn:Xn;...;x1:X1]];
-[mind_entry_arity] is [Ai], defined in context [[[x1:X1;...;xn:Xn]];
-[mind_entry_lc] is [Ti1;...;Tini], defined in context [[A'1;...;A'p;x1:X1;...;xn:Xn]] where [A'i] is [Ai] generalized over [[x1:X1;...;xn:Xn]].
-*)
-
-type one_inductive_entry = {
-  mind_entry_typename : identifier;
-  mind_entry_arity : constr;
-  mind_entry_consnames : identifier list;
-  mind_entry_lc : constr list }
-
-type mutual_inductive_entry = {
-  mind_entry_record : bool;
-  mind_entry_finite : bool;
-  mind_entry_params : (identifier * local_entry) list;
-  mind_entry_inds : one_inductive_entry list }
-
-
-(*s Constants (Definition/Axiom) *)
-
-type definition_entry = {
-  const_entry_body   : constr;
-  const_entry_secctx : section_context option;
-  const_entry_type   : types option;
-  const_entry_opaque : bool }
-
-type inline = int option (* inlining level, None for no inlining *)
-
-type parameter_entry = section_context option * types * inline 
-
-type constant_entry =
-  | DefinitionEntry of definition_entry
-  | ParameterEntry of parameter_entry
-
-(*s Modules *)
-
-type module_struct_entry =
-    MSEident of module_path
-  | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry
-  | MSEwith of module_struct_entry * with_declaration
-  | MSEapply of module_struct_entry * module_struct_entry
-
-and with_declaration =
-    With_Module of identifier list * module_path
-  | With_Definition of identifier list * constr
-
-and module_entry =
-    { mod_entry_type : module_struct_entry option;
-      mod_entry_expr : module_struct_entry option}
-
-
diff --git a/kernel/entries.mli b/kernel/entries.mli
deleted file mode 100644
index 2460ec6445..0000000000
--- a/kernel/entries.mli
+++ /dev/null
@@ -1,83 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Univ
-open Term
-open Sign
-
-(** This module defines the entry types for global declarations. This
-   information is entered in the environments. This includes global
-   constants/axioms, mutual inductive definitions, modules and module
-   types *)
-
-
-(** {6 Local entries } *)
-
-type local_entry =
-  | LocalDef of constr
-  | LocalAssum of constr
-
-
-(** {6 Declaration of inductive types. } *)
-
-(** Assume the following definition in concrete syntax:
-{v Inductive I1 (x1:X1) ... (xn:Xn) : A1 := c11 : T11 | ... | c1n1 : T1n1
-...
-with      Ip (x1:X1) ... (xn:Xn) : Ap := cp1 : Tp1 | ... | cpnp : Tpnp. v}
-
-then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
-[mind_entry_arity] is [Ai], defined in context [x1:X1;...;xn:Xn];
-[mind_entry_lc] is [Ti1;...;Tini], defined in context [[A'1;...;A'p;x1:X1;...;xn:Xn]] where [A'i] is [Ai] generalized over [[x1:X1;...;xn:Xn]].
-*)
-
-type one_inductive_entry = {
-  mind_entry_typename : identifier;
-  mind_entry_arity : constr;
-  mind_entry_consnames : identifier list;
-  mind_entry_lc : constr list }
-
-type mutual_inductive_entry = {
-  mind_entry_record : bool;
-  mind_entry_finite : bool;
-  mind_entry_params : (identifier * local_entry) list;
-  mind_entry_inds : one_inductive_entry list }
-
-(** {6 Constants (Definition/Axiom) } *)
-
-type definition_entry = {
-  const_entry_body   : constr;
-  const_entry_secctx : section_context option;
-  const_entry_type   : types option;
-  const_entry_opaque : bool }
-
-type inline = int option (* inlining level, None for no inlining *)
-
-type parameter_entry = section_context option * types * inline 
-
-type constant_entry =
-  | DefinitionEntry of definition_entry
-  | ParameterEntry of parameter_entry
-
-(** {6 Modules } *)
-
-type module_struct_entry =
-    MSEident of module_path
-  | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry
-  | MSEwith of module_struct_entry * with_declaration
-  | MSEapply of module_struct_entry * module_struct_entry
-
-and with_declaration =
-    With_Module of identifier list * module_path
-  | With_Definition of identifier list * constr
-
-and module_entry =
-    { mod_entry_type : module_struct_entry option;
-      mod_entry_expr : module_struct_entry option}
-
-
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 8c1dd53adc..872a6c9054 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -16,7 +16,6 @@ Conv_oracle
 Closure
 Reduction
 Type_errors
-Entries
 Modops
 Inductive
 Typeops
-- 
cgit v1.2.3