From df49e6b29fa9e8ac971c3e08f20ae6cb0f5b9889 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 27 Jul 2017 00:01:26 +0200 Subject: [api] Fix base_include LTAC parts. --- dev/base_include | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev/base_include') diff --git a/dev/base_include b/dev/base_include index bfbf6bb5d..79ecd73e0 100644 --- a/dev/base_include +++ b/dev/base_include @@ -194,8 +194,8 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;; let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; +let parse_tac = API.Pcoq.parse_string Ltac_plugin.Pltac.tactic;; (* build a term of type glob_constr without type-checking or resolution of implicit syntax *) -- cgit v1.2.3