From ead31bf3e2fe220d02dec59dce66471cc2c66fce Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 11 Aug 2003 10:25:04 +0000
Subject: 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
---
 tactics/eauto.ml4     |  2 +-
 tactics/extraargs.ml4 |  4 +++-
 tactics/tacinterp.ml  | 12 +++++++++---
 3 files changed, 13 insertions(+), 5 deletions(-)

(limited to 'tactics')

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
-- 
cgit v1.2.3