diff options
| author | sacerdot | 2004-11-17 17:44:35 +0000 |
|---|---|---|
| committer | sacerdot | 2004-11-17 17:44:35 +0000 |
| commit | 9a5c5db122becb63c5b72a967ef141bdd3fb5319 (patch) | |
| tree | 456513517718198461fabae4e96242348aeeab13 /contrib/interface | |
| parent | 85500252f0e8c0d2b2cceb2418bcadadbbc5cfd0 (diff) | |
New command "Print Rewrite HindDb dbname".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/ascent.mli | 1 | ||||
| -rw-r--r-- | contrib/interface/vtp.ml | 3 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 2 |
3 files changed, 6 insertions, 0 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index 88ffb2bcee..dfe64d2274 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -124,6 +124,7 @@ and ct_COMMAND = | CT_print_graph | CT_print_hint of ct_ID_OPT | CT_print_hintdb of ct_ID_OR_STAR + | CT_print_rewrite_hintdb of ct_ID | CT_print_id of ct_ID | CT_print_implicit of ct_ID | CT_print_loadpath diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 48047cf96f..ebad140808 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -418,6 +418,9 @@ and fCOMMAND = function | CT_print_hintdb(x1) -> fID_OR_STAR x1; fNODE "print_hintdb" 1 +| CT_print_rewrite_hintdb(x1) -> + fID x1; + fNODE "print_rewrite_hintdb" 1 | CT_print_id(x1) -> fID x1; fNODE "print_id" 1 diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index a997e30958..b0a0f4977c 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1768,6 +1768,8 @@ let rec xlate_vernac = | 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)) + | PrintRewriteHintDbName id -> + CT_print_rewrite_hintdb (CT_ident id) | PrintHint id -> CT_print_hint (CT_coerce_ID_to_ID_OPT (loc_qualid_to_ct_ID id)) | PrintHintGoal -> CT_print_hint ctv_ID_OPT_NONE |