From 087430f522a57beea37a296f0cffa1a3d1f49fed Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 3 Oct 2001 14:12:52 +0000
Subject: 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
---
 kernel/typeops.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 3e8de823a6..4342b5793e 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
 
-- 
cgit v1.2.3