From 01cd0dd64e4faa52b5094a99e2c31ecc4e7b767d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 02:09:54 +0100
Subject: Moving Print Ltac to an EXTEND based command.

---
 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 3b5d276dd2..0ad39d8047 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -890,7 +890,6 @@ GEXTEND Gram
       | IDENT "Classes" ->  PrintClasses
       | IDENT "TypeClasses" -> PrintTypeClasses
       | IDENT "Instances"; qid = smart_global -> PrintInstances qid
-      | IDENT "Ltac"; qid = global -> PrintLtac qid
       | IDENT "Coercions" -> PrintCoercions
       | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
          -> PrintCoercionPaths (s,t)
-- 
cgit v1.2.3