bugs avec Pose et Assert

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

3 files changed, 13 insertions, 11 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index ed4417797b..1da57f9209 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -216,9 +216,9 @@ let pr_let_binder pr x a =
          pr_sep_com (fun () -> brk(0,1)) (pr ltop) a)
 
 let rec extract_prod_binders = function
-  | CLetIn (loc,na,b,c) as x ->
+(*  | CLetIn (loc,na,b,c) as x ->
       let bl,c = extract_prod_binders c in
-      if bl = [] then [], x else LocalRawDef (na,b) :: bl, c
+      if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
   | CProdN (loc,[],c) ->
       extract_prod_binders c
   | CProdN (loc,(nal,t)::bl,c) ->
@@ -227,9 +227,9 @@ let rec extract_prod_binders = function
   | c -> [], c
 
 let rec extract_lam_binders = function
-  | CLetIn (loc,na,b,c) as x ->
+(*  | CLetIn (loc,na,b,c) as x ->
       let bl,c = extract_lam_binders c in
-      if bl = [] then [], x else LocalRawDef (na,b) :: bl, c
+      if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
   | CLambdaN (loc,[],c) ->
       extract_lam_binders c
   | CLambdaN (loc,(nal,t)::bl,c) ->
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index a6ff11b0e4..5e0cc68bac 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -483,9 +483,9 @@ and pr_atom1 env = function
       hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
              str"with " ++ prlist_with_sep spc (pr_cofix_tac env) l)
   | TacCut c -> hov 1 (str "cut" ++ pr_constrarg env c)
-  | TacTrueCut (None,c) -> 
+  | TacTrueCut (Anonymous,c) -> 
       hov 1 (str "assert" ++ pr_constrarg env c)
-  | TacTrueCut (Some id,c) -> 
+  | TacTrueCut (Name id,c) -> 
       hov 1 (str "assert" ++ spc () ++
              hov 1 (str"(" ++ pr_id id ++ str " :" ++
                     pr_lconstrarg env c ++ str")"))
@@ -495,7 +495,7 @@ and pr_atom1 env = function
                     pr_lconstrarg env c ++ str")"))
   | TacForward (true,Anonymous,c) ->
       if Options.do_translate () then
-        (* Pose was buggy and was wrongly substituting in conclusion in v7 *)
+        (* Pose was buggy and was wrongly substituted in conclusion in v7 *)
         hov 1 (str "set" ++ pr_constrarg env c)
       else
         hov 1 (str "pose" ++ pr_constrarg env c)
@@ -514,7 +514,9 @@ and pr_atom1 env = function
   | TacGeneralizeDep c ->
       hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
              pr_constrarg env c)
-  | TacLetTac (id,c,cl) ->
+  | TacLetTac (Anonymous,c,cl) ->
+      hov 1 (str "set" ++ pr_constrarg env c) ++ pr_clauses pr_ident cl
+  | TacLetTac (Name id,c,cl) ->
       hov 1 (str "set" ++ spc () ++
              hov 1 (str"(" ++ pr_id id ++ str " :=" ++
                     pr_lconstrarg env c ++ str")") ++
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 41f36ccda4..6756e3157f 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -824,16 +824,16 @@ let rec pr_vernac = function
   | VernacRecord (b,(oc,name),ps,s,c,fs) ->
       let pr_record_field = function
         | (oc,AssumExpr (id,t)) ->
-            hov 1 (pr_lident id ++
+            hov 1 (pr_lname id ++
             (if oc then str" :>" else str" :") ++ spc() ++
             pr_type t)
         | (oc,DefExpr(id,b,opt)) -> (match opt with
 	    | Some t ->
-                hov 1 (pr_lident id ++
+                hov 1 (pr_lname id ++
                 (if oc then str" :>" else str" :") ++ spc() ++
                 pr_type t ++ str" :=" ++ pr_lconstr b)
 	    | None ->
-                hov 1 (pr_lident id ++ str" :=" ++ spc() ++
+                hov 1 (pr_lname id ++ str" :=" ++ spc() ++
                 pr_lconstr b)) in
       hov 2
         (str (if b then "Record" else "Structure") ++