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.

---
 parsing/g_vernac.ml4 | 1 -
 1 file changed, 1 deletion(-)

(limited to 'parsing')

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