- module Redinfo dans library/ pour les constantes d'élimination

 - module Tacred : fonctions de reductions utilisees dans les tactiques


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@114 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 1 deletions

diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 421aa9aaf..585a57344 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -25,11 +25,14 @@ type 'a stack_reduction_function =
 val whd_stack : 'a stack_reduction_function
 
 (*s Reduction Function Operators *)
+
 val under_casts : 'a reduction_function -> 'a reduction_function
 val strong : 'a reduction_function -> 'a reduction_function
 val strong_prodspine : 'a reduction_function -> 'a reduction_function
 val stack_reduction_of_reduction : 
   'a reduction_function -> 'a stack_reduction_function
+val stacklam : (constr -> constr list -> 'a) -> constr list -> constr 
+  -> constr list -> 'a 
 
 (*s Generic Optimized Reduction Functions using Closures *)
 
@@ -57,6 +60,7 @@ val whd_betadeltaiota_stack : 'a stack_reduction_function
 
 
 (*s Head normal forms *)
+
 val whd_const_stack : section_path list -> 'a stack_reduction_function
 val whd_const : section_path list -> 'a reduction_function
 val whd_delta_stack : 'a stack_reduction_function
@@ -67,12 +71,13 @@ val whd_betadeltat_stack : 'a stack_reduction_function
 val whd_betadeltat : 'a reduction_function
 val whd_betadeltatiota_stack : 'a stack_reduction_function
 val whd_betadeltatiota : 'a reduction_function
+val whd_betadeltaeta_stack : 'a stack_reduction_function
+val whd_betadeltaeta : 'a reduction_function
 val whd_betadeltaiotaeta_stack : 'a stack_reduction_function
 val whd_betadeltaiotaeta : 'a reduction_function
 
 val beta_applist : (constr * constr list) -> constr
 
-
 val hnf_prod_app : 
   unsafe_env -> 'a evar_map -> string -> constr -> constr -> constr
 val hnf_prod_appvect : 
@@ -91,6 +96,16 @@ val decomp_prod : unsafe_env -> 'a evar_map -> constr -> int * constr
 val decomp_n_prod : 
   unsafe_env -> 'a evar_map -> int -> constr -> ((name * constr) list) * constr
 
+type 'a miota_args = {
+  mP      : constr;     (* the result type *)
+  mconstr : constr;     (* the constructor *)
+  mci     : case_info;  (* special info to re-build pattern *)
+  mcargs  : 'a list;    (* the constructor's arguments *)
+  mlf     : 'a array }  (* the branch code vector *)
+
+val reducible_mind_case : constr -> bool
+val reduce_mind_case : unsafe_env -> constr miota_args -> constr
+
 val is_arity : unsafe_env -> 'a evar_map -> constr -> bool
 val is_info_arity : unsafe_env -> 'a evar_map -> constr -> bool
 val is_info_sort : unsafe_env -> 'a evar_map -> constr -> bool
@@ -111,6 +126,9 @@ val subst_term_occ : int list -> constr -> constr -> constr
 val pattern_occs : (int list * constr * constr) list -> 'a reduction_function
 val compute : 'a reduction_function
 
+val fix_recarg : constr -> 'a list -> (int * 'a) option
+val reduce_fix : (constr -> 'a list -> constr * constr list) -> constr ->
+  constr list -> bool * (constr * constr list)
 
 (*s Conversion Functions (uses closures, lazy strategy) *)
 
@@ -185,4 +203,5 @@ val minductype_spec : unsafe_env -> 'a evar_map -> constr -> constr
 val mrectype_spec : unsafe_env -> 'a evar_map -> constr -> constr
 
 (* Special function, which keep the key casts under Fix and MutCase. *)
+
 val strip_all_casts : constr -> constr