diff options
| author | Pierre-Marie Pédrot | 2016-03-06 23:00:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-06 23:06:12 +0100 |
| commit | ffac73b8f3f3bf6877ce652eecac7849b7c2a182 (patch) | |
| tree | c309ce25302e1851fc5442ee95b7d4f36589d6ef /toplevel | |
| parent | cdc91f02f98b4d857bfebe61d95b920787a8d0e5 (diff) | |
Moving Autorewrite to Hightatctic.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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)) |