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

---
 checker/closure.mli | 33 +++++++++++++++++++++------------
 1 file changed, 21 insertions(+), 12 deletions(-)

(limited to 'checker/closure.mli')

diff --git a/checker/closure.mli b/checker/closure.mli
index e072a106..e6b39250 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -1,15 +1,14 @@
 (************************************************************************)
 (*  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        *)
 (************************************************************************)
 
 (*i*)
-open Pp
 open Names
-open Term
+open Cic
 open Esubst
 open Environ
 (*i*)
@@ -25,7 +24,7 @@ val with_stats: 'a Lazy.t -> 'a
   Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
   a LetIn expression is Letin reduction *)
 
-type transparent_state = Idpred.t * Cpred.t
+type transparent_state = Id.Pred.t * Cpred.t
 
 val all_opaque      : transparent_state
 val all_transparent : transparent_state
@@ -44,7 +43,7 @@ module type RedFlagsSig = sig
   val fIOTA : red_kind
   val fZETA : red_kind
   val fCONST : constant -> red_kind
-  val fVAR : identifier -> red_kind
+  val fVAR : Id.t -> red_kind
 
   (* No reduction at all *)
   val no_red : reds
@@ -67,11 +66,13 @@ val betaiotazeta       : reds
 val betadeltaiotanolet : reds
 
 (***********************************************************************)
-type table_key =
-  | ConstKey of constant
-  | VarKey of identifier
+type 'a tableKey =
+  | ConstKey of 'a
+  | VarKey of Id.t
   | RelKey of int
 
+type table_key = constant puniverses tableKey
+
 type 'a infos
 val ref_value_cache: 'a infos -> table_key -> 'a option
 val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos
@@ -91,12 +92,14 @@ type fterm =
   | FAtom of constr (* Metas and Sorts *)
   | FCast of fconstr * cast_kind * fconstr
   | FFlex of table_key
-  | FInd of inductive
-  | FConstruct of constructor
+  | FInd of pinductive
+  | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
+  | FProj of constant * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
-  | FCases of case_info * fconstr * fconstr * fconstr array
+  | FCase of case_info * fconstr * fconstr * fconstr array
+  | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
   | FLambda of int * (name * constr) list * constr * fconstr subs
   | FProd of name * fconstr * fconstr
   | FLetIn of name * fconstr * fconstr * constr * fconstr subs
@@ -113,6 +116,8 @@ type fterm =
 type stack_member =
   | Zapp of fconstr array
   | Zcase of case_info * fconstr * fconstr array
+  | ZcaseT of case_info * constr * constr array * fconstr subs
+  | Zproj of int * int * constant
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
@@ -121,6 +126,9 @@ and stack = stack_member list
 
 val append_stack : fconstr array -> stack -> stack
 val eta_expand_stack : stack -> stack
+ 
+val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> 
+   (fconstr * stack) -> stack * stack
 
 (* To lazy reduce a constr, create a [clos_infos] with
    [create_clos_infos], inject the term to reduce with [inject]; then use
@@ -136,6 +144,8 @@ val destFLambda :
 (* Global and local constant cache *)
 type clos_infos
 val create_clos_infos : reds -> env -> clos_infos
+val infos_env : clos_infos -> env
+val infos_flags : clos_infos -> reds
 
 (* Reduction function *)
 
@@ -172,6 +182,5 @@ val kni: clos_infos -> fconstr -> stack -> fconstr * stack
 val knr: clos_infos -> fconstr -> stack -> fconstr * stack
 
 val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
-val optimise_closure : fconstr subs -> constr -> fconstr subs * constr
 
 (* End of cbn debug section i*)
-- 
cgit v1.2.3