From 1682d4ed9df64937dfaa162e58233020036ff7b3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 Feb 2017 13:23:15 +0100
Subject: Fixing #use"include" after vernac is added and ltac is moved to a
 plugin.

---
 dev/base_include | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 0abcefc38e..242405ae29 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -17,7 +17,7 @@
 #directory "grammar";;
 #directory "intf";;
 #directory "stm";;
-#directory "ltac";;
+#directory "vernac";;
 
 #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
 #directory "+camlp5";; (* Gramext is found in top_printers.ml *)
@@ -195,7 +195,7 @@ let qid = Libnames.qualid_of_string;;
 (* parsing of terms *)
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_tac    = Pcoq.parse_string Pltac.tactic;;
+let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
-- 
cgit v1.2.3