From ffac73b8f3f3bf6877ce652eecac7849b7c2a182 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Mar 2016 23:00:58 +0100
Subject: Moving Autorewrite to Hightatctic.

---
 printing/ppvernac.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'printing')

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"
-- 
cgit v1.2.3