diff options
Diffstat (limited to 'translate/ppvernacnew.ml')
| -rw-r--r-- | translate/ppvernacnew.ml | 9 |
1 files changed, 6 insertions, 3 deletions
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) -> |