*** empty log message ***

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

2 files changed, 21 insertions, 8 deletions

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) ->