Depliage des let-in dans le test de garde

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

3 files changed, 13 insertions, 11 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 272ecc57d7..3447a5741f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -159,6 +159,7 @@ open RedFlags
 let beta = mkflags [fbeta]
 let betaevar = mkflags [fevar; fbeta]
 let betaiota = mkflags [fiota; fbeta]
+let betaiotazeta = mkflags [fiota; fbeta;fzeta]
 
 (* Contextual *)
 let delta = mkflags [fdelta;fevar]
@@ -399,6 +400,12 @@ let whd_betaiota_stack x =
 let whd_betaiota x =
   app_stack (whd_betaiota_state (x, empty_stack))
 
+let whd_betaiotazeta_state = local_whd_state_gen betaiotazeta
+let whd_betaiotazeta_stack x =
+  appterm_of_stack (whd_betaiotazeta_state (x, empty_stack))
+let whd_betaiotazeta x =
+  app_stack (whd_betaiotazeta_state (x, empty_stack))
+
 let whd_betaiotaevar_state e = whd_state_gen betaiotaevar e
 let whd_betaiotaevar_stack env sigma x =
   appterm_of_stack (whd_betaiotaevar_state env sigma (x, empty_stack))
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index a32f36a6af..09d47fec9f 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -65,18 +65,21 @@ val nf_betadeltaiota : 'a reduction_function
 (* Lazy strategy, weak head reduction *)
 val whd_beta : local_reduction_function
 val whd_betaiota : local_reduction_function
+val whd_betaiotazeta : local_reduction_function
 val whd_betadeltaiota : 'a contextual_reduction_function
 val whd_betadeltaiota_nolet : 'a contextual_reduction_function
 val whd_betaetalet : local_reduction_function
 
 val whd_beta_stack : local_stack_reduction_function
 val whd_betaiota_stack : local_stack_reduction_function
+val whd_betaiotazeta_stack : local_stack_reduction_function
 val whd_betadeltaiota_stack : 'a contextual_stack_reduction_function
 val whd_betadeltaiota_nolet_stack : 'a contextual_stack_reduction_function
 val whd_betaetalet_stack : local_stack_reduction_function
 
 val whd_beta_state : local_state_reduction_function
 val whd_betaiota_state : local_state_reduction_function
+val whd_betaiotazeta_state : local_state_reduction_function
 val whd_betadeltaiota_state : 'a contextual_state_reduction_function
 val whd_betadeltaiota_nolet_state : 'a contextual_state_reduction_function
 val whd_betaetalet_state : local_state_reduction_function
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 63d4ed069b..3eef05bf0a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -590,7 +590,7 @@ let rec check_subterm_rec_meta env sigma vectn k def =
      (* n gives the index of the recursive variable *)
      (noccur_with_meta (n+k+1) nfi t) or 
      (* no recursive call in the term *)
-     (let f,l = whd_betaiota_stack t in
+     (let f,l = whd_betaiotazeta_stack t in
       match kind_of_term f with
 	| IsRel p -> 
 	    if n+k+1 <= p & p < n+k+nfi+1 then
@@ -675,16 +675,8 @@ let rec check_subterm_rec_meta env sigma vectn k def =
 	       (n+1) (map_lift_fst lst) b) &&
             (List.for_all (check_rec_call env n lst) l)
 
-	| IsLetIn (x,a,b,c) as cst -> 
-	    (try 
-	    (check_rec_call env n lst a) &&
-	    (check_rec_call env n lst b) &&
-            (check_rec_call (push_rel_def (x,a, b) env)
-	       (n+1) (map_lift_fst lst) c) &&
-            (List.for_all (check_rec_call env n lst) l)
-	    with (FixGuardError NotEnoughArgumentsForFixCall) as e
-		-> check_rec_call env n lst (whd_betadeltaiota env sigma t)
-            )
+	| IsLetIn (x,a,b,c) -> 
+	    anomaly "check_rec_call: should have been reduced"
 
 	| IsMutInd (_,la) -> 
 	     (array_for_all (check_rec_call env n lst) la) &&