diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-03 14:12:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-03 14:12:52 +0000 |
| commit | 087430f522a57beea37a296f0cffa1a3d1f49fed (patch) | |
| tree | da2b09ea5c32a73e5851693b4644df624e0035ff /kernel/typeops.ml | |
| parent | 2096151b12d5565771aefcc4c87726ce367ae50c (diff) | |
Bugs de vérification de la bonne fondation en présence de définitions locales dans le type de l'inductif décroissant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2099 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 3e8de823a..4342b5793 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -465,6 +465,9 @@ let check_term env mind_recvec f = (List.map (instantiate_recarg sp lrc)) sprecargs.(i) in crec env' n' ((1,lc)::lst') (lr,b) | _ -> crec env' n' lst' (lr,b) end + | (_,IsLetIn (x,c,a,b)) -> + let env' = push_rel_def (x,c,a) env in + crec env' (n+1) (map_lift_fst lst) (lrec,(subst1 c b)) | (_,_) -> f env n lst c' in crec env |