diff options
| author | herbelin | 2001-07-03 16:25:27 +0000 |
|---|---|---|
| committer | herbelin | 2001-07-03 16:25:27 +0000 |
| commit | c155881b687667746474f5f2b13be2c4f347838d (patch) | |
| tree | 1333564c7a1f4651eec11465722df3daa6a9b9db /kernel/typeops.ml | |
| parent | ca9b228384584e125a146b68157180d229a5914e (diff) | |
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
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 14 |
1 files changed, 3 insertions, 11 deletions
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) && |