Nouvelle mouture du traducteur v7->v8

Option -v8 à coqtop lance coqtopnew
Le terminateur reste "." en v8
Ajout construction primitive CLetTuple/RLetTuple
Introduction typage dans le traducteur pour traduire les Case/Cases/Match
Ajout mutables dans RCases or ROrderedCase pour permettre la traduction
Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts
+ Bugs ou améliorations diverses
Raffinement affichage projections de Record/Structure.


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

3 files changed, 13 insertions, 5 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 2bd30c5ebc..ddd5e42203 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -358,7 +358,7 @@ open Genarg
 let pr_hintbases _prc _prt = function 
   | None -> str " with *"
   | Some [] -> mt ()
-  | Some l -> str " with " ++ Util.prlist str l
+  | Some l -> str " with " ++ Util.prlist_with_sep spc str l
 
 ARGUMENT EXTEND hintbases
   TYPED AS preident_list_opt
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 37b8b33564..2a2db30f83 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -19,7 +19,9 @@ open Genarg
 let _ = Metasyntax.add_token_obj "<-"
 let _ = Metasyntax.add_token_obj "->"
 
-let pr_orient _prc _prt = function true -> Pp.str " ->" | false -> Pp.str " <-"
+let pr_orient _prc _prt = function
+  | true -> Pp.mt ()
+  | false -> Pp.str " <-"
 
 ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
 | [ "->" ] -> [ true ]
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9462a7423f..2efdabafc1 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -408,8 +408,14 @@ let intern_constr {ltacvars=lfun; gsigma=sigma; genv=env} c =
   let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
   let c' = 
     warn (Constrintern.interp_rawconstr_gen false sigma env []
-           false (fst lfun,[])) c
-  in (c',if !strict_check then None else Some c)
+           false (fst lfun,[])) c in
+  begin if Options.do_translate () then try
+      (* Try to infer old case and type annotations *)
+      let _ = Pretyping.understand_gen_tcc sigma env [] None c' in 
+      (* msgerrnl (str "Typage tactique OK");*)
+      ()
+    with e -> (*msgerrnl (str "Warning: can't type tactic");*) () end;
+  (c',if !strict_check then None else Some c)
 
 (* Globalize bindings *)
 let intern_binding ist (loc,b,c) =
@@ -2014,7 +2020,7 @@ let make_empty_glob_sign () =
     gsigma = Evd.empty; genv = Global.env() }
 
 let add_tacdef isrec tacl =
-  let isrec = if !Options.p1 then isrec else true in
+(*  let isrec = if !Options.p1 then isrec else true in*)
   let rfun = List.map (fun ((loc,id as locid),_) -> (id,make_absolute_name locid)) tacl in
   let ist =
     {(make_empty_glob_sign()) with ltacrecvars = if isrec then rfun else []} in