diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 825e8d549..cd0fb899c 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -37,7 +37,7 @@ type printable = | PrintFullContext | PrintSectionContext of reference | PrintInspect of int - | PrintGrammar of string * string + | PrintGrammar of string | PrintLoadPath | PrintModules | PrintModule of reference |