- Correction d'un bug de de Bruijn dans abstract_predicate (lié au

  rapport de bug #1671 - mais ne résoud pas le #1671 dans le propos peut
  être vu comme le souhait de voir traité le cas simple du problème
  généralement indécidable d'inversion des contraintes des types 
  inductifs)
- Petite amélioration dans le nommage des variables dans expand_arg



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

1 files changed, 7 insertions, 7 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index f8c8e0a138..e76a9745a5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -996,18 +996,18 @@ let abstract_predicate env sigma indf cur tms = function
       (* Depending on whether the predicate is dependent or not, and has real
          args or not, we lift it to make room for [sign] *)
       (* Even if not intrinsically dep, we move the predicate into a dep one *)
-      let sign,k =
+      let sign,q =
         if names = [] & n <> 1 then
           (* Real args were not considered *)
           (if dep<>Anonymous then
-            ((let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign),n-1)
+            (let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign)
           else
-            (sign,n))
+            sign),n
         else
           (* Real args are OK *)
-          (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign,
-           if dep<>Anonymous then 0 else 1) in
-      let pred = lift_predicate k pred in
+          (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign,1) in
+      let q,k = if dep <> Anonymous then (q-1,2) else (q,1) in
+      let pred = liftn_predicate q k pred in
       let pred = extract_predicate [] (pred,tms) in
       (true, it_mkLambda_or_LetIn_name env pred sign)
 
@@ -1026,7 +1026,7 @@ 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
+    if alreadydep<>Anonymous then if na <> Anonymous then na else 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