aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernac.ml')
-rw-r--r--toplevel/vernac.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 84acc9bfa..14e4b8eb7 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -234,7 +234,7 @@ let set_formatter_translator() =
let pr_new_syntax loc ocom =
let loc = Loc.unloc loc in
if !beautify_file then set_formatter_translator();
- let fs = States.freeze () in
+ let fs = States.freeze ~marshallable:false in
let com = match ocom with
| Some VernacNop -> mt()
| Some com -> Ppvernac.pr_vernac com