From 699b70cd9ad0d79cbde228bdb51fde224a3b524e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 14 Sep 2016 17:19:14 +0200
Subject: Moving Ltac-specific parsing API to ltac/ folder.

---
 dev/base_include | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index b09b6df2de..0abcefc38e 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -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 Pcoq.Tactic.tactic;;
+let parse_tac    = Pcoq.parse_string 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