nouvel algo de conversion plus uniforme

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

1 files changed, 10 insertions, 5 deletions

diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 9ac3d8042..50371e85f 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -16,15 +16,11 @@ open Environ
 (***********************************************************************)
 (*s Reduction functions *)
 
+val whd_betaiotazeta        : env -> constr -> constr
 val whd_betadeltaiota       : env -> constr -> constr
 val whd_betadeltaiota_nolet : env -> constr -> constr
 
 val nf_betaiota      : constr -> constr
-val hnf_stack        : env -> constr -> constr * constr list
-val hnf_prod_applist : env -> types -> constr list -> types
-
-(* Builds an application node, reducing beta redexes it may produce. *) 
-val beta_appvect : constr -> constr array -> constr
 
 (***********************************************************************)
 (*s conversion functions *)
@@ -38,6 +34,15 @@ val conv_leq       : types conversion_function
 val conv_leq_vecti : types array conversion_function
 
 (***********************************************************************)
+
+(* Builds an application node, reducing beta redexes it may produce. *) 
+val beta_appvect : constr -> constr array -> constr
+
+(* Pseudo-reduction rule  Prod(x,A,B) a --> B[x\a] *)
+val hnf_prod_applist : env -> types -> constr list -> types
+
+
+(***********************************************************************)
 (*s Recognizing products and arities modulo reduction *)
 
 val dest_prod       : env -> types -> Sign.rel_context * types