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. --- plugins/ssrmatching/ssrmatching.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ssrmatching') diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 5fb0bb6647..150be9d727 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -41,7 +41,7 @@ open Proofview.Notations open Tacinterp open Pretyping open Constr -open Tactic +open Pltac open Extraargs open Ppconstr open Printer -- cgit v1.2.3