diff options
| -rw-r--r-- | contrib/interface/xlate.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index bf5aed32e8..0bcaa47eb0 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1792,7 +1792,7 @@ let rec xlate_vernac = | PrintOpaqueName id -> CT_print_opaqueid (loc_qualid_to_ct_ID id) | PrintSectionContext id -> CT_print_section (loc_qualid_to_ct_ID id) | PrintModules -> CT_print_modules - | PrintGrammar (phylum, name) -> CT_print_grammar CT_grammar_none + | PrintGrammar name -> CT_print_grammar CT_grammar_none | PrintHintDb -> CT_print_hintdb (CT_coerce_STAR_to_ID_OR_STAR CT_star) | PrintHintDbName id -> CT_print_hintdb (CT_coerce_ID_to_ID_OR_STAR (CT_ident id)) diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 825e8d5494..cd0fb899ca 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 |