reparation de qqs bugs du traducteur

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

3 files changed, 15 insertions, 10 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 1da57f9209..8a2ce3765b 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -262,11 +262,14 @@ let split_product na' = function
       rename na na' t (CProdN(loc,(nal,t)::bl,c))
   | _ -> anomaly "ill-formed fixpoint body"
 
-let merge_binders (na1,ty1) (na2,ty2) =
+let merge_binders (na1,ty1) (na2,ty2) codom =
   let na =
     match snd na1, snd na2 with
         Anonymous, Name id -> na2
-      | Name id, Anonymous -> na1
+      | Name id, Anonymous ->
+          if occur_var_constr_expr id codom then
+            failwith "avoid capture"
+          else na1
       | Anonymous, Anonymous -> na1
       | Name id1, Name id2 ->
           if id1 <> id2 then failwith "not same name" else na1 in
@@ -277,18 +280,18 @@ let merge_binders (na1,ty1) (na2,ty2) =
       | _ ->
           Constrextern.check_same_type ty1 ty2;
           ty2 in
-  LocalRawAssum ([na],ty)
+  (LocalRawAssum ([na],ty), codom)
             
 let rec strip_domain bvar c =
   match c with
     | CArrow(loc,a,b) ->
-        (merge_binders bvar ((dummy_loc,Anonymous),a), b)
+        merge_binders bvar ((dummy_loc,Anonymous),a) b
     | CProdN(loc,[([na],ty)],c') ->
-        (merge_binders bvar (na,ty), c')
+        merge_binders bvar (na,ty) c'
     | CProdN(loc,([na],ty)::bl,c') ->
-        (merge_binders bvar (na,ty), CProdN(loc,bl,c'))
+        merge_binders bvar (na,ty) (CProdN(loc,bl,c'))
     | CProdN(loc,(na::nal,ty)::bl,c') ->
-        (merge_binders bvar (na,ty), CProdN(loc,(nal,ty)::bl,c'))
+        merge_binders bvar (na,ty) (CProdN(loc,(nal,ty)::bl,c'))
     | _ -> failwith "not a product"
 
 (* Note: binder sharing is lost *)
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index b4002994fe..63423b7b52 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -145,7 +145,7 @@ let id_of_ltac_v7_id id =
 let pr_ltac_or_var pr = function
   | ArgArg x -> pr x
   | ArgVar (loc,id) ->
-      pr_with_comments loc (Nameops.pr_id (id_of_ltac_v7_id id))
+      pr_with_comments loc (pr_id (id_of_ltac_v7_id id))
 
 let pr_arg pr x = spc () ++ pr x
 
@@ -331,9 +331,9 @@ let pr_seq_body pr tl =
 
 let duplicate force pr = function
   | [] -> pr (ref false,[])
-  | [x] -> pr x
+  | x::l when List.for_all (fun y -> snd x=snd y) l -> pr x
   | l ->
-      if List.exists (fun (b,ids) -> !b) l & (force or
+     if List.exists (fun (b,ids) -> !b) l & (force or
 	 List.exists (fun (_,ids) -> ids <> (snd (List.hd l))) (List.tl l))
       then pr_seq_body pr (List.rev l)
       else pr (ref false,[])
diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli
index b6861f8160..88f57f61ab 100644
--- a/translate/pptacticnew.mli
+++ b/translate/pptacticnew.mli
@@ -24,3 +24,5 @@ val pr_glob_tactic : Environ.env -> glob_tactic_expr -> std_ppcmds
 val pr_tactic : Environ.env -> Proof_type.tactic_expr -> std_ppcmds
 
 val id_of_ltac_v7_id : identifier -> identifier
+
+