diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-24 15:14:28 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-24 15:14:28 +0000 |
commit | 8eeec81e418603eaffc295bf20744da91b2e0f83 (patch) | |
tree | 18b25f058250616c8a6688568c0969273385a77e | |
parent | 67c294eba2b62b1cc0ffa8fe01687ea99bb1d64c (diff) |
Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9678 85f007b7-540e-0410-9357-904b9bb8a0f7
-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 bf5aed32e..0bcaa47eb 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 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 |