diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index b52af04f3..b0b26b33c 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -139,6 +139,8 @@ let rec vernac_com interpfun (loc,com) = | VernacV7only _ -> Options.v7_only := true; if !translate_file then msg (pr_comments !comments) + | VernacNop -> + if !translate_file then msg (pr_comments !comments) | _ -> let fs = States.freeze () in if !translate_file then |