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

---
 checker/cic.mli | 32 ++++++++++----------------------
 1 file changed, 10 insertions(+), 22 deletions(-)

(limited to 'checker/cic.mli')

diff --git a/checker/cic.mli b/checker/cic.mli
index c4b00d0d..17259bb4 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -33,11 +33,10 @@ open Names
 
 (** {6 The sorts of CCI. } *)
 
-type contents = Pos | Null
-
 type sorts =
-  | Prop of contents       (** Prop and Set *)
-  | Type of Univ.universe  (** Type *)
+  | Prop
+  | Set
+  | Type of Univ.universe
 
 (** {6 The sorts family of CCI. } *)
 
@@ -128,7 +127,7 @@ type section_context = unit
 (** {6 Substitutions} *)
 
 type delta_hint =
-  | Inline of int * constr option
+  | Inline of int * (Univ.AUContext.t * constr) option
   | Equiv of KerName.t
 
 type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t
@@ -203,18 +202,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 : constr; (* Type under params *)
-  proj_eta : constr * constr; (* Eta-expanded term and type *)
-  proj_body : constr; (* For compatibility, the match version *)
-}
-
 type constant_def =
   | Undef of inline
   | Def of constr_substituted
@@ -233,6 +220,7 @@ type typing_flags = {
                             points are assumed to be total. *)
   check_universes : bool; (** If [false] universe constraints are not checked *)
   conv_oracle : oracle; (** Unfolding strategies for conversion *)
+  share_reduction : bool; (** Use by-need reduction algorithm *)
 }
 
 type constant_body = {
@@ -241,7 +229,6 @@ type constant_body = {
     const_type : constr;
     const_body_code : to_patch_substituted;
     const_universes : constant_universes;
-    const_proj : projection_body option;
     const_inline_code : bool;
     const_typing_flags : typing_flags;
 }
@@ -255,9 +242,10 @@ type recarg =
 
 type wf_paths = recarg Rtree.t
 
-type record_body = (Id.t * Constant.t array * projection_body array) option
-    (* The body is empty for non-primitive records, otherwise we get its
-       binder name in projections and list of projections if it is primitive. *)
+type record_info =
+| NotRecord
+| FakeRecord
+| PrimRecord of (Id.t * Label.t array * constr array) array
 
 type regular_inductive_arity = {
   mind_user_arity : constr;
@@ -325,7 +313,7 @@ type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
 
-    mind_record : record_body option; (** Whether the inductive type has been declared as a record. *)
+    mind_record : record_info; (** Whether the inductive type has been declared as a record. *)
 
     mind_finite : recursivity_kind;  (** Whether the type is inductive or coinductive *)
 
-- 
cgit v1.2.3