diff options
| -rw-r--r-- | intf/vernacexpr.mli | 1 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 1 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 2 | ||||
| -rw-r--r-- | tactics/g_rewrite.ml4 | 4 | ||||
| -rw-r--r-- | tactics/hightactics.mllib | 1 | ||||
| -rw-r--r-- | tactics/tactics.mllib | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 1 |
7 files changed, 5 insertions, 6 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 7273b92b9a..5501ca7c7f 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -69,7 +69,6 @@ type printable = | PrintHint of reference or_by_notation | PrintHintGoal | PrintHintDbName of string - | PrintRewriteHintDbName of string | PrintHintDb | PrintScopes | PrintScope of string diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b5e9f9e067..49baeb5560 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -951,7 +951,6 @@ GEXTEND Gram | IDENT "Hint"; qid = smart_global -> PrintHint qid | IDENT "Hint"; "*" -> PrintHintDb | IDENT "HintDb"; s = IDENT -> PrintHintDbName s - | "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s | IDENT "Scopes" -> PrintScopes | IDENT "Scope"; s = IDENT -> PrintScope s | IDENT "Visibility"; s = OPT [x = IDENT -> x ] -> PrintVisibility s diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index ffec926a84..a101540aba 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -486,8 +486,6 @@ module Make keyword "Print Hint *" | PrintHintDbName s -> keyword "Print HintDb" ++ spc () ++ str s - | PrintRewriteHintDbName s -> - keyword "Print Rewrite HintDb" ++ spc() ++ str s | PrintUniverses (b, fopt) -> let cmd = if b then "Print Sorted Universes" diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index 72cfb01a57..6b6dc7b21a 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -261,3 +261,7 @@ TACTIC EXTEND setoid_transitivity [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ] | [ "setoid_etransitivity" ] -> [ setoid_transitivity None ] END + +VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY + [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Pp.msg_notice (Autorewrite.print_rewrite_hintdb s) ] +END diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib index 0d73cc27aa..73f11d0be0 100644 --- a/tactics/hightactics.mllib +++ b/tactics/hightactics.mllib @@ -1,5 +1,6 @@ Extraargs Coretactics +Autorewrite Extratactics Eauto G_auto diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index eebac88fba..fd7fab0c58 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -25,5 +25,4 @@ Tactic_debug Tacinterp Evar_tactics Term_dnet -Autorewrite Tactic_option diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d769c60332..c63dac3026 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1629,7 +1629,6 @@ let vernac_print = function | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r)) | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s) - | PrintRewriteHintDbName s -> msg_notice (Autorewrite.print_rewrite_hintdb s) | PrintHintDb -> msg_notice (Hints.pr_searchtable ()) | PrintScopes -> msg_notice (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr)) |