From 811ed22e8dcb12d8c88e2c320bbc2221bdff30ab Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 3 Oct 2017 15:09:21 +0200
Subject: Implementing a generic mechanism for locating named objects from Coq
 side.

---
 parsing/g_vernac.ml4 | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 819d236cd3..3e0b85b54a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1020,8 +1020,7 @@ GEXTEND Gram
       | IDENT "Term"; qid = smart_global -> LocateTerm qid
       | IDENT "File"; f = ne_string -> LocateFile f
       | IDENT "Library"; qid = global -> LocateLibrary qid
-      | IDENT "Module"; qid = global -> LocateModule qid
-      | IDENT "Ltac"; qid = global -> LocateTactic qid ] ]
+      | IDENT "Module"; qid = global -> LocateModule qid ] ]
   ;
   option_value:
     [ [ n  = integer   -> IntValue (Some n)
-- 
cgit v1.2.3