From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 kernel/declarations.ml | 43 ++++++++++++++++++++-----------------------
 1 file changed, 20 insertions(+), 23 deletions(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index b7427d20..61fcb483 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -46,18 +46,6 @@ type inline = int option
 (** A constant can have no body (axiom/parameter), or a
     transparent body, or an opaque one *)
 
-(** Projections are a particular kind of constant: 
-    always transparent. *)
-
-type projection_body = {
-  proj_ind : MutInd.t;
-  proj_npars : int;
-  proj_arg : int;
-  proj_type : types; (* Type under params *)
-  proj_eta : constr * types; (* Eta-expanded term and type *)
-  proj_body : constr; (* For compatibility with VMs only, the match version *)
-}
-
 (* Global declarations (i.e. constants) can be either: *)
 type constant_def =
   | Undef of inline                       (** a global assumption *)
@@ -77,17 +65,17 @@ type typing_flags = {
                             points are assumed to be total. *)
   check_universes : bool; (** If [false] universe constraints are not checked *)
   conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *)
+  share_reduction : bool; (** Use by-need reduction algorithm *)
 }
 
 (* some contraints are in constant_constraints, some other may be in
  * the OpaqueDef *)
 type constant_body = {
-    const_hyps : Context.Named.t; (** New: younger hyp at top *)
+    const_hyps : Constr.named_context; (** New: younger hyp at top *)
     const_body : constant_def;
     const_type : types;
     const_body_code : Cemitcodes.to_patch_substituted option;
     const_universes : constant_universes;
-    const_proj : projection_body option;
     const_inline_code : bool;
     const_typing_flags : typing_flags; (** The typing options which
                                            were used for
@@ -112,13 +100,22 @@ v}
 *)
 
 (** Record information:
-    If the record is not primitive, then None
-    Otherwise, we get:
+    If the type is not a record, then NotRecord
+    If the type is a non-primitive record, then FakeRecord
+    If it is a primitive record, for every type in the block, we get:
     - The identifier for the binder name of the record in primitive projections.
     - The constants associated to each projection.
-    - The checked projection bodies. *)
+    - The projection types (under parameters).
+
+    The kernel does not exploit the difference between [NotRecord] and
+    [FakeRecord]. It is mostly used by extraction, and should be extruded from
+    the kernel at some point.
+*)
 
-type record_body = (Id.t * Constant.t array * projection_body array) option
+type record_info =
+| NotRecord
+| FakeRecord
+| PrimRecord of (Id.t * Label.t array * types array) array
 
 type regular_inductive_arity = {
   mind_user_arity : types;
@@ -132,7 +129,7 @@ type one_inductive_body = {
 
     mind_typename : Id.t; (** Name of the type: [Ii] *)
 
-    mind_arity_ctxt : Context.Rel.t; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
+    mind_arity_ctxt : Constr.rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
 
     mind_arity : inductive_arity; (** Arity sort and original user arity *)
 
@@ -167,7 +164,7 @@ type one_inductive_body = {
 
     mind_nb_args : int; (** number of no constant constructor *)
 
-    mind_reloc_tbl :  Cbytecodes.reloc_table;
+    mind_reloc_tbl :  Vmvalues.reloc_table;
   }
 
 type abstract_inductive_universes =
@@ -184,19 +181,19 @@ type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
 
-    mind_record : record_body option; (** The record information *)
+    mind_record : record_info; (** The record information *)
 
     mind_finite : recursivity_kind;  (** Whether the type is inductive or coinductive *)
 
     mind_ntypes : int;  (** Number of types in the block *)
 
-    mind_hyps : Context.Named.t;  (** Section hypotheses on which the block depends *)
+    mind_hyps : Constr.named_context;  (** Section hypotheses on which the block depends *)
 
     mind_nparams : int;  (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *)
 
     mind_nparams_rec : int;  (** Number of recursively uniform (i.e. ordinary) parameters *)
 
-    mind_params_ctxt : Context.Rel.t;  (** The context of parameters (includes let-in declaration) *)
+    mind_params_ctxt : Constr.rel_context;  (** The context of parameters (includes let-in declaration) *)
 
     mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *)
 
-- 
cgit v1.2.3