From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 kernel/reduction.mli | 43 +++++++++++++++++++++++++++++--------------
 1 file changed, 29 insertions(+), 14 deletions(-)

(limited to 'kernel/reduction.mli')

diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 8a2b2469..49384340 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -1,12 +1,14 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Term
+open Constr
 open Environ
 
 (***********************************************************************
@@ -35,20 +37,26 @@ type 'a extended_conversion_function =
 
 type conv_pb = CONV | CUMUL
 
-type 'a universe_compare = 
-  { (* Might raise NotConvertible or UnivInconsistency *)
-    compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
-    compare_instances: flex:bool -> 
-		       Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
-  } 
+type 'a universe_compare =
+  { (* Might raise NotConvertible *)
+    compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
+    compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+    compare_cumul_instances : conv_pb -> Univ.Variance.t array ->
+      Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a }
 
 type 'a universe_state = 'a * 'a universe_compare
 
 type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b
 
-type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints
+type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
 
-val sort_cmp_universes : env -> conv_pb -> sorts -> sorts ->
+val get_cumulativity_constraints : conv_pb -> Univ.Variance.t array ->
+  Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t
+
+val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int
+val constructor_cumulativity_arguments : (Declarations.mutual_inductive_body * int * int) -> int
+
+val sort_cmp_universes : env -> conv_pb -> Sorts.t -> Sorts.t ->
   'a * 'a universe_compare -> 'a * 'a universe_compare
 
 (* [flex] should be true for constants, false for inductive types and
@@ -100,6 +108,12 @@ val beta_app : constr -> constr -> constr
 (** Pseudo-reduction rule  Prod(x,A,B) a --> B[x\a] *)
 val hnf_prod_applist : env -> types -> constr list -> types
 
+(** In [hnf_prod_applist_assum n c args], [c] is supposed to (whd-)reduce to
+    the form [∀Γ.t] with [Γ] of length [n] and possibly with let-ins; it
+    returns [t] with the assumptions of [Γ] instantiated by [args] and
+    the local definitions of [Γ] expanded. *)
+val hnf_prod_applist_assum : env -> int -> types -> constr list -> types
+
 (** Compatibility alias for Term.lambda_appvect_assum *)
 val betazeta_appvect : int -> constr -> constr array -> constr
 
@@ -108,11 +122,12 @@ val betazeta_appvect : int -> constr -> constr array -> constr
 
 val dest_prod       : env -> types -> Context.Rel.t * types
 val dest_prod_assum : env -> types -> Context.Rel.t * types
+val dest_lam        : env -> types -> Context.Rel.t * constr
 val dest_lam_assum  : env -> types -> Context.Rel.t * types
 
 exception NotArity
 
-val dest_arity : env -> types -> arity (* raises NotArity if not an arity *)
+val dest_arity : env -> types -> Term.arity (* raises NotArity if not an arity *)
 val is_arity   : env -> types -> bool
 
 val warn_bytecode_compiler_failed : ?loc:Loc.t -> unit -> unit
-- 
cgit v1.2.3