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.

---
 intf/vernacexpr.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'intf')

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