*** empty log message ***

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

3 files changed, 43 insertions, 18 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7aae0f38d4..f5410a8a16 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -124,12 +124,14 @@ let set_formatter_translator() =
 
 let pre_printing = function
   | VernacSolve (i,tac,deftac) when Options.do_translate () ->
-      let (_,env) = Pfedit.get_goal_context i in
-      let t = Options.with_option Options.translate_syntax
-	(Tacinterp.glob_tactic_env [] env) tac in
-      let pfts = Pfedit.get_pftreestate () in
-      let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in
-      Some (env,t,Pfedit.focus(),List.length gls)
+      (try
+        let (_,env) = Pfedit.get_goal_context i in
+        let t = Options.with_option Options.translate_syntax
+	  (Tacinterp.glob_tactic_env [] env) tac in
+        let pfts = Pfedit.get_pftreestate () in
+        let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in
+        Some (env,t,Pfedit.focus(),List.length gls)
+      with UserError _|Stdpp.Exc_located _ -> None)
   | _ -> None
 
 let post_printing loc (env,t,f,n) = function
@@ -213,10 +215,20 @@ let rec vernac_com interpfun (loc,com) =
   in 
   try
     Options.v7_only := false;
-    let pp = pre_printing com in
-    if pp = None & do_translate() then pr_new_syntax loc (Some com);
-    interp com;
-    if pp <> None & do_translate() then post_printing loc (out_some pp) com
+    if do_translate () then
+      match pre_printing com with
+          None ->
+            pr_new_syntax loc (Some com);
+            interp com
+        | Some state ->
+            (try
+              interp com;
+              post_printing loc state com
+            with e ->
+              post_printing loc state com;
+              raise e)
+    else
+      interp com
   with e -> 
     Format.set_formatter_out_channel stdout;
     Options.v7_only := false;
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index e0c8331ffb..9ff326b522 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -40,6 +40,11 @@ let strip_prod_binders_expr n ty =
       | _ -> error "Cannot translate fix tactic: not enough products" in
   strip_ty [] n ty
 
+let is_ident_expr = function
+    Topconstr.CRef(Ident _) -> true
+  | _ -> false
+
+
 (* In v8 syntax only double quote char is escaped by repeating it *)
 let rec escape_string_v8 s =
   let rec escape_at s i =
@@ -369,7 +374,7 @@ let pr_then () = str ";"
 
 open Closure
 
-let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,strip_prod_binders) =
+let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,strip_prod_binders,is_ident) =
 
 let pr_bindings env = pr_bindings (pr_lconstr env) (pr_constr env) in
 let pr_ex_bindings env = pr_bindings_gen true (pr_lconstr env) (pr_constr env) in
@@ -744,7 +749,8 @@ let rec pr_tac env inherited tac =
       pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom
   | TacArg(Tacexp e) -> pr_tac0 env e, latom
   | TacArg(ConstrMayEval (ConstrTerm c)) ->
-      str "constr:" ++ pr_constr env c, latom
+      if is_ident c then pr_constr env c, latom
+      else str "constr:" ++ pr_constr env c, latom
   | TacArg(ConstrMayEval c) ->
       pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c, leval
   | TacArg(TacFreshId sopt) -> str "fresh" ++ pr_opt qsnew sopt, latom
@@ -789,6 +795,10 @@ let strip_prod_binders_rawterm n (ty,_) =
         | _ -> error "Cannot translate fix tactic: not enough products" in
   strip_ty [] n ty
 
+let is_ident_rawterm = function
+    (Rawterm.RRef(_,VarRef _),_) -> true
+  | _ -> false
+
 let strip_prod_binders_constr n ty =
   let rec strip_ty acc n ty =
     if n=0 then (List.rev acc, ty) else
@@ -810,7 +820,7 @@ let rec raw_printers =
      pr_reference,
      pr_or_metaid (pr_located pr_id),
      Pptactic.pr_raw_extend,
-     strip_prod_binders_expr)
+     strip_prod_binders_expr, is_ident_expr)
 
 and pr_raw_tactic env (t:raw_tactic_expr) =
   pi1 (make_pr_tac raw_printers) env t
@@ -835,7 +845,7 @@ let rec glob_printers =
      pr_ltac_or_var (pr_located pr_ltac_constant),
      pr_located pr_id,
      Pptactic.pr_glob_extend,
-     strip_prod_binders_rawterm)
+     strip_prod_binders_rawterm, is_ident_rawterm)
 
 and pr_glob_tactic env (t:glob_tactic_expr) =
   pi1 (make_pr_tac glob_printers) env t
@@ -858,5 +868,5 @@ let (pr_tactic,_,_) =
      pr_ltac_constant,
      pr_id,
      Pptactic.pr_extend,
-     strip_prod_binders_constr)
+     strip_prod_binders_constr,Term.isVar)
 
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 4d78ee179a..2612a59254 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -447,7 +447,8 @@ let pr_syntax_entry (p,rl) =
 let pr_vernac_solve (i,env,tac,deftac) =
   (if i = 1 then mt() else int i ++ str ": ") ++
   Pptacticnew.pr_glob_tactic env tac
-  ++ (if deftac & Pfedit.get_end_tac() <> None then str ".." else mt ())
+  ++ (try if deftac & Pfedit.get_end_tac() <> None then str ".." else mt ()
+      with UserError _|Stdpp.Exc_located _ -> mt())
 
 (**************************************)
 (* Pretty printer for vernac commands *)
@@ -877,10 +878,12 @@ let rec pr_vernac = function
   (* Solving *)
   | VernacSolve (i,tac,deftac) ->
       (* Normally shunted by vernac.ml *)
-      let (_,env) = Pfedit.get_goal_context i in
+      let env =
+        try snd (Pfedit.get_goal_context i)
+        with UserError _ -> Global.env() in
       let tac = 
 	Options.with_option Options.translate_syntax 
-	  (Tacinterp.glob_tactic_env [] env) tac in
+	  (Constrintern.for_grammar (Tacinterp.glob_tactic_env [] env)) tac in
       pr_vernac_solve (i,env,tac,deftac)
 
   | VernacSolveExistential (i,c) ->