From 675884d2e03507602f4149eec7917d047b82e941 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 15 May 2001 06:40:28 +0000
Subject: Correction bug predicat du Cases (suite)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1752 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index df06b4f701..b207f4247f 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -932,7 +932,7 @@ let weaken_predicate q pred =
 	  let copt, p = if dep then Some (mkRel (q+k)), 1 else None, 0 in
           (* PrNotInd is a binding iff copt <> None *)
 	  PrNotInd (copt, weakrec (n-1) (k+p) pred)
-  in weakrec q 0 pred
+  in weakrec q 0 (lift_predicate q pred)
 
 (*****************************************************************************)
 (* pred = [X:=realargs;x:=e]P types the following problem:                   *)
-- 
cgit v1.2.3