Correction du bug de build_initial_predicate a révèlé un autre bug dans expand_arg

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6457 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 2 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 9d336fc24..3f149293b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -980,6 +980,13 @@ let rec map_predicate f k = function
       let k' = List.length names + (if dep<>Anonymous then 1 else 0) in
       PrLetIn (tm, map_predicate f (k+k') pred)
 
+let rec noccurn_predicate k = function
+  | PrCcl ccl -> noccurn k ccl
+  | PrProd pred -> noccurn_predicate (k+1) pred
+  | PrLetIn ((names,dep as tm),pred) ->
+      let k' = List.length names + (if dep<>Anonymous then 1 else 0) in
+      noccurn_predicate (k+k') pred
+
 let liftn_predicate n = map_predicate (liftn n)
 
 let lift_predicate n = liftn_predicate n 1
@@ -1091,8 +1098,9 @@ let rec known_dependent = function
 let expand_arg n alreadydep (na,t) deps (k,pred) =
   (* current can occur in pred even if the original problem is not dependent *)
   let dep =
-    if alreadydep<>Anonymous then alreadydep else
-    if deps <> [] then Name (id_of_string "x") else Anonymous in
+    if alreadydep<>Anonymous then alreadydep
+    else if deps = [] && noccurn_predicate 1 pred then Anonymous
+    else Name (id_of_string "x") in
   let pred = if dep<>Anonymous then pred else lift_predicate (-1) pred in
   (* There is no dependency in realargs for subpattern *)
   (k-1, PrLetIn (([],dep), pred))