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/constr.mli | 41 +++++++++++++++++++++++++++++++----------
 1 file changed, 31 insertions(+), 10 deletions(-)

(limited to 'kernel/constr.mli')

diff --git a/kernel/constr.mli b/kernel/constr.mli
index c1d1f988..70acf193 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -161,8 +161,26 @@ val mkCase : case_info * constr * constr * constr array -> constr
 
    where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
 *)
-type rec_declaration = Name.t array * types array * constr array
-type fixpoint = (int array * int) * rec_declaration
+type ('constr, 'types) prec_declaration =
+    Name.t array * 'types array * 'constr array
+type ('constr, 'types) pfixpoint =
+    (int array * int) * ('constr, 'types) prec_declaration
+  (* The array of [int]'s tells for each component of the array of
+     mutual fixpoints the number of lambdas to skip before finding the
+     recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B)
+     (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is
+     the recursive argument);
+     The second component [int] tells which component of the block is
+     returned *)
+
+type ('constr, 'types) pcofixpoint =
+    int * ('constr, 'types) prec_declaration
+  (* The component [int] tells which component of the block of
+     cofixpoint is returned *)
+
+type rec_declaration = (constr, types) prec_declaration
+
+type fixpoint = (constr, types) pfixpoint
 val mkFix : fixpoint -> constr
 
 (** If [funnames = [|f1,.....fn|]]
@@ -176,7 +194,7 @@ val mkFix : fixpoint -> constr
      ...
      with       fn = bn.]
  *)
-type cofixpoint = int * rec_declaration
+type cofixpoint = (constr, types) pcofixpoint
 val mkCoFix : cofixpoint -> constr
 
 
@@ -185,12 +203,6 @@ val mkCoFix : cofixpoint -> constr
 (** [constr array] is an instance matching definitional [named_context] in
    the same order (i.e. last argument first) *)
 type 'constr pexistential = Evar.t * 'constr array
-type ('constr, 'types) prec_declaration =
-    Name.t array * 'types array * 'constr array
-type ('constr, 'types) pfixpoint =
-    (int array * int) * ('constr, 'types) prec_declaration
-type ('constr, 'types) pcofixpoint =
-    int * ('constr, 'types) prec_declaration
 
 type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Rel       of int                                  (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *)
@@ -360,6 +372,15 @@ val eq_constr_nounivs : constr -> constr -> bool
 (** Total ordering compatible with [equal] *)
 val compare : constr -> constr -> int
 
+(** {6 Extension of Context with declarations on constr} *)
+
+type rel_declaration = (constr, types) Context.Rel.Declaration.pt
+type named_declaration = (constr, types) Context.Named.Declaration.pt
+type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt
+type rel_context = rel_declaration list
+type named_context = named_declaration list
+type compacted_context = compacted_declaration list
+
 (** {6 Functionals working on the immediate subterm of a construction } *)
 
 (** [fold f acc c] folds [f] on the immediate subterms of [c]
@@ -422,7 +443,7 @@ val compare_head : constr_compare_fn -> constr_compare_fn
 (** Convert a global reference applied to 2 instances. The int says
    how many arguments are given (as we can only use cumulativity for
    fully applied inductives/constructors) .*)
-type instance_compare_fn = global_reference -> int ->
+type instance_compare_fn = GlobRef.t -> int ->
   Univ.Instance.t -> Univ.Instance.t -> bool
 
 (** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to
-- 
cgit v1.2.3