Essai de suppression de eta dans simpl (cf bug #779)

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

3 files changed, 15 insertions, 7 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 8ebc170df6..5acb766581 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -157,6 +157,7 @@ let betadeltaiota_nolet = mkflags [fbeta;fdelta;fevar;fiota]
 let betadeltaiotaeta = mkflags [fbeta;fdelta;fzeta;fevar;fiota;feta]
 let betaiotaevar = mkflags [fbeta;fiota;fevar]
 let betaetalet = mkflags [fbeta;feta;fzeta]
+let betalet = mkflags [fbeta;fzeta]
 
 (* Beta Reduction tools *)
 
@@ -350,6 +351,10 @@ let whd_betaetalet_stack x =
   appterm_of_stack (whd_betaetalet_state (x, empty_stack))
 let whd_betaetalet x = app_stack (whd_betaetalet_state (x,empty_stack))
 
+let whd_betalet_state = local_whd_state_gen betalet
+let whd_betalet_stack x = appterm_of_stack (whd_betalet_state (x, empty_stack))
+let whd_betalet x = app_stack (whd_betalet_state (x,empty_stack))
+
 (* 2. Delta Reduction Functions *)
 
 let whd_delta_state e = whd_state_gen delta e
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 2a76441ad1..87dba7a197 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -71,6 +71,7 @@ val whd_betaiotazeta : local_reduction_function
 val whd_betadeltaiota :  contextual_reduction_function
 val whd_betadeltaiota_nolet :  contextual_reduction_function
 val whd_betaetalet : local_reduction_function
+val whd_betalet : local_reduction_function
 
 val whd_beta_stack : local_stack_reduction_function
 val whd_betaiota_stack : local_stack_reduction_function
@@ -78,6 +79,7 @@ val whd_betaiotazeta_stack : local_stack_reduction_function
 val whd_betadeltaiota_stack :  contextual_stack_reduction_function
 val whd_betadeltaiota_nolet_stack :  contextual_stack_reduction_function
 val whd_betaetalet_stack : local_stack_reduction_function
+val whd_betalet_stack : local_stack_reduction_function
 
 val whd_state : local_state_reduction_function
 val whd_beta_state : local_state_reduction_function
@@ -86,6 +88,7 @@ val whd_betaiotazeta_state : local_state_reduction_function
 val whd_betadeltaiota_state :  contextual_state_reduction_function
 val whd_betadeltaiota_nolet_state :  contextual_state_reduction_function
 val whd_betaetalet_state : local_state_reduction_function
+val whd_betalet_state : local_state_reduction_function
 
 (*s Head normal forms *)
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 792291d997..0bf4b6a608 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -208,7 +208,7 @@ let invert_name labs l na0 env sigma ref = function
 		| None -> None
 		| Some c -> 
 		    let labs',ccl = decompose_lam c in
-		    let _, l' = whd_betaetalet_stack ccl in
+		    let _, l' = whd_betalet_stack ccl in
 		    let labs' = List.map snd labs' in
 		    if labs' = labs & l = l' then Some ref else None
       else Some ref
@@ -220,7 +220,7 @@ let invert_name labs l na0 env sigma ref = function
 
 let compute_consteval_direct sigma env ref =
   let rec srec env n labs c =
-    let c',l = whd_betadeltaeta_stack env sigma c in
+    let c',l = whd_betadelta_stack env sigma c in
     match kind_of_term c' with
       | Lambda (id,t,g) when l=[] ->
 	  srec (push_rel (id,None,t) env) (n+1) (t::labs) g
@@ -236,7 +236,7 @@ let compute_consteval_direct sigma env ref =
 
 let compute_consteval_mutual_fix sigma env ref =
   let rec srec env minarg labs ref c =
-    let c',l = whd_betaetalet_stack c in
+    let c',l = whd_betalet_stack c in
     let nargs = List.length l in
     match kind_of_term c' with
       | Lambda (na,t,g) when l=[] ->
@@ -419,12 +419,12 @@ let rec red_elim_const env sigma ref largs =
   match reference_eval sigma env ref with
     | EliminationCases n when stack_args_size largs >= n ->
 	let c = reference_value sigma env ref in
-	let c', lrest = whd_betadeltaeta_state env sigma (c,largs) in
+	let c', lrest = whd_betadelta_state env sigma (c,largs) in
         (special_red_case sigma env (construct_const env sigma) (destCase c'),
 	 lrest)
     | EliminationFix (min,infos) when stack_args_size largs >=min ->
 	let c = reference_value sigma env ref in
-	let d, lrest = whd_betadeltaeta_state env sigma (c,largs) in
+	let d, lrest = whd_betadelta_state env sigma (c,largs) in
 	let f = make_elim_fun ([|Some ref|],infos) largs in
 	let co = construct_const env sigma in
 	(match reduce_fix_use_function f co (destFix d) lrest with
@@ -437,10 +437,10 @@ let rec red_elim_const env sigma ref largs =
 	  if ref = refgoal then
 	    (c,args)
 	  else
-	    let c', lrest = whd_betaetalet_state (c,args) in
+	    let c', lrest = whd_betalet_state (c,args) in
 	    descend (destEvalRef c') lrest in
 	let (_, midargs as s) = descend ref largs in
-	let d, lrest = whd_betadeltaeta_state env sigma s in
+	let d, lrest = whd_betadelta_state env sigma s in
 	let f = make_elim_fun refinfos midargs in
 	let co = construct_const env sigma in
 	(match reduce_fix_use_function f co (destFix d) lrest with