lettac -> set

suppression de la notation carre de R


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

2 files changed, 31 insertions, 27 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 281ca2c5c..7e71f5623 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -394,12 +394,14 @@ let rec pr inherited a =
   | CRef r -> pr_reference r, latom
   | CFix (_,id,fix) ->
       let p = hov 0 (str"fix " ++ pr_recursive (pr_fixdecl pr) (snd id) fix) in
-      (if List.length fix = 1 & prec_less (fst inherited) ltop
-       then surround p else p),
-      lfix
+      if List.length fix = 1 & prec_less (fst inherited) ltop
+      then surround p, latom else p, lfix
   | CCoFix (_,id,cofix) ->
-      hov 0 (str "cofix " ++ pr_recursive (pr_cofixdecl pr) (snd id) cofix),
-      lfix
+      let p =
+        hov 0 (str "cofix " ++
+               pr_recursive (pr_cofixdecl pr) (snd id) cofix) in
+      if List.length cofix = 1 & prec_less (fst inherited) ltop
+      then surround p, latom else p, lfix
   | CArrow (_,a,b) ->
       hov 0 (pr (larrow,L) a ++ str " ->" ++ brk(1,0) ++ pr (-larrow,E) b),
       larrow
@@ -504,9 +506,6 @@ let rec pr inherited a =
         str "end"),
       latom
   | CHole _ -> str "_", latom
-(*
-  | CEvar (_,n) -> str "?" ++ int n, latom
-*)
   | CEvar (_,n) -> str (Evd.string_of_existential n), latom
   | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
   | CSort (_,s) -> pr_sort s, latom
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index f36e053fc..cf8c57ae9 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -362,16 +362,15 @@ let pr_fix_tac env (id,n,c) =
   let annot =
     if List.length names = 1 then mt()
     else spc() ++ str"{struct " ++ pr_id idarg ++ str"}" in
-  spc() ++ str"with " ++
-  hov 0 (pr_id id ++ 
-        prlist (pr_binder_fix env) bll ++ annot ++ str" :" ++ spc() ++
-        pr_lconstr env ty) in
+  hov 1 (str"(" ++ pr_id id ++ 
+        prlist (pr_binder_fix env) bll ++ annot ++ str" :" ++
+        pr_lconstrarg env ty ++ str")") in
 (*  spc() ++
   hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
     env c)
 *)
 let pr_cofix_tac env (id,c) =
-  spc() ++ str"with " ++ hov 0 (pr_id id ++ str":" ++ pr_constrarg env c) in
+  hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg env c ++ str")") in
 
 
   (* Printing tactics as arguments *)
@@ -421,26 +420,29 @@ and pr_atom1 env = function
   | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg env c)
   | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
   | TacMutualFix (id,n,l) ->
-      hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++
-             prlist (pr_fix_tac env) l)
+      hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ cut() ++
+             str"with " ++ prlist_with_sep spc (pr_fix_tac env) l)
   | TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido)
   | TacMutualCofix (id,l) ->
-      hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc () ++
-             prlist (pr_cofix_tac env) l)
+      hov 1 (str "cofix" ++ spc () ++ pr_id id ++ cut () ++
+             str"with " ++ prlist_with_sep spc (pr_cofix_tac env) l)
   | TacCut c -> hov 1 (str "cut" ++ pr_constrarg env c)
   | TacTrueCut (None,c) -> 
       hov 1 (str "assert" ++ pr_constrarg env c)
   | TacTrueCut (Some id,c) -> 
-      hov 1 (str "assert" ++ spc () ++ str"(" ++ pr_id id ++ str ":" ++
-             pr_lconstrarg env c ++ str")")
+      hov 1 (str "assert" ++ spc () ++
+             hov 1 (str"(" ++ pr_id id ++ str " :" ++
+                    pr_lconstrarg env c ++ str")"))
   | TacForward (false,na,c) ->
-      hov 1 (str "assert" ++ spc () ++ str"(" ++ pr_name na ++ str " :=" ++
-             pr_lconstrarg env c ++ str")")
+      hov 1 (str "assert" ++ spc () ++
+             hov 1 (str"(" ++ pr_name na ++ str " :=" ++
+                    pr_lconstrarg env c ++ str")"))
   | TacForward (true,Anonymous,c) ->
       hov 1 (str "pose" ++ pr_constrarg env c)
   | TacForward (true,Name id,c) ->
-      hov 1 (str "pose" ++ spc() ++ str"(" ++ pr_id id ++ str " :=" ++
-             pr_lconstrarg env c ++ str")")
+      hov 1 (str "pose" ++ spc() ++
+             hov 1 (str"(" ++ pr_id id ++ str " :=" ++
+                    pr_lconstrarg env c ++ str")"))
   | TacGeneralize l ->
       hov 1 (str "generalize" ++ spc () ++
              prlist_with_sep spc (pr_constr env) l)
@@ -448,11 +450,14 @@ and pr_atom1 env = function
       hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
              pr_constrarg env c)
   | TacLetTac (id,c,cl) ->
-      hov 1 (str "lettac" ++ spc () ++ str"(" ++ pr_id id ++ str " :=" ++
-        pr_lconstrarg env c ++ str")" ++ pr_clause_pattern pr_ident cl)
+      hov 1 (str "set" ++ spc () ++
+             hov 1 (str"(" ++ pr_id id ++ str " :=" ++
+                    pr_lconstrarg env c ++ str")") ++
+             pr_clause_pattern pr_ident cl)
   | TacInstantiate (n,c) ->
-      hov 1 (str "instantiate" ++ str"(" ++ pr_arg int n ++ str":=" ++
-             pr_lconstrarg env c ++ str")")
+      hov 1 (str "instantiate" ++ spc() ++
+             hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+                    pr_lconstrarg env c ++ str")"))
 
   (* Derived basic tactics *)
   | TacSimpleInduction h ->