diff options
| -rw-r--r-- | toplevel/vernac.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index b325c8b192..51357950e1 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -143,13 +143,14 @@ let rec vernac_com interpfun (loc,com) = if !translate_file then msg (pr_comments !comments) | _ -> let fs = States.freeze () in + let p = pr_vernac com in if !translate_file then - msgnl (pr_comments !comments ++ hov 0 (pr_vernac com)) + msgnl (pr_comments !comments ++ hov 0 p) else (msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ pr_comments !comments ++ - pr_vernac com)); - States.unfreeze fs)); + p))); + States.unfreeze fs); Constrintern.set_temporary_implicits_in []; Constrextern.set_temporary_implicits_out []; comments := None; |