From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 kernel/entries.mli | 67 +++++++++++++++++++++++++++++++++---------------------
 1 file changed, 41 insertions(+), 26 deletions(-)

(limited to 'kernel/entries.mli')

diff --git a/kernel/entries.mli b/kernel/entries.mli
index 5782d092..303d27d3 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -1,15 +1,13 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \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
@@ -37,47 +35,64 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
 *)
 
 type one_inductive_entry = {
-  mind_entry_typename : identifier;
+  mind_entry_typename : Id.t;
   mind_entry_arity : constr;
-  mind_entry_consnames : identifier list;
+  mind_entry_template : bool; (* Use template polymorphism *)
+  mind_entry_consnames : Id.t 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 }
+  mind_entry_record : (Id.t option) option; 
+  (** Some (Some id): primitive record with id the binder name of the record
+      in projections.
+      Some None: non-primitive record *)
+  mind_entry_finite : Decl_kinds.recursivity_kind;
+  mind_entry_params : (Id.t * local_entry) list;
+  mind_entry_inds : one_inductive_entry list;
+  mind_entry_polymorphic : bool; 
+  mind_entry_universes : Univ.universe_context;
+  mind_entry_private : bool option }
 
 (** {6 Constants (Definition/Axiom) } *)
+type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects
+type const_entry_body = proof_output Future.computation
 
 type definition_entry = {
-  const_entry_body   : constr;
-  const_entry_secctx : section_context option;
-  const_entry_type   : types option;
-  const_entry_opaque : bool }
+  const_entry_body   : const_entry_body;
+  (* List of section variables *)
+  const_entry_secctx : Context.section_context option;
+  (* State id on which the completion of type checking is reported *)
+  const_entry_feedback : Stateid.t option;
+  const_entry_type        : types option;
+  const_entry_polymorphic : bool;
+  const_entry_universes   : Univ.universe_context;
+  const_entry_opaque      : bool;
+  const_entry_inline_code : bool }
 
 type inline = int option (* inlining level, None for no inlining *)
 
-type parameter_entry = section_context option * types * inline 
+type parameter_entry = 
+    Context.section_context option * bool * types Univ.in_universe_context * inline 
+
+type projection_entry = {
+  proj_entry_ind : mutual_inductive;
+  proj_entry_arg : int }
 
 type constant_entry =
   | DefinitionEntry of definition_entry
   | ParameterEntry of parameter_entry
+  | ProjectionEntry of projection_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
+type module_struct_entry = Declarations.module_alg_expr
 
-and module_entry =
-    { mod_entry_type : module_struct_entry option;
-      mod_entry_expr : module_struct_entry option}
+type module_params_entry =
+  (MBId.t * module_struct_entry) list (** older first *)
 
+type module_type_entry = module_params_entry * module_struct_entry
 
+type module_entry =
+  | MType of module_params_entry * module_struct_entry
+  | MExpr of
+      module_params_entry * module_struct_entry * module_struct_entry option
-- 
cgit v1.2.3