From 2e62e97ac5b63dfe2ea97f4da4e341b8ef6eed5d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 13 Apr 2004 12:19:03 +0000
Subject: Correction confusion entre la dependance en les termes filtrees dans
 l'annotation donnee par l'utilisateur et l'annotation utilisee en interne

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5668 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cases.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0084fce652..dbd52f5702 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1609,12 +1609,12 @@ let build_initial_predicate isdep pred tomatchl =
     | [] -> PrCcl pred
     | tm::ltm ->
         let nrealargs = cook tm in
-        let pred, p =
+        let pred, p, user_p =
           if isdep then 
-            if dependent (mkRel (nar-n)) pred then pred, 1
-            else liftn (-1) (nar-n) pred, 0
-          else pred, 0 in
-	PrLetIn ((nrealargs,p=1), buildrec (n+nrealargs+p) pred ltm)
+            if dependent (mkRel (nar-n)) pred then pred, 1, 1
+            else liftn (-1) (nar-n) pred, 0, 1
+          else pred, 0, 0 in
+	PrLetIn ((nrealargs,p=1), buildrec (n+nrealargs+user_p) pred ltm)
   in buildrec 0 pred tomatchl
 
 let extract_arity_signature env0 tomatchl tmsign =
-- 
cgit v1.2.3