From 0437339ccac602d692b5b8c071b77ac756805520 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 15 Jun 2017 16:41:09 +0200 Subject: Removing Proof_type from the API. Unluckily, this forces replacing a lot of code in plugins, because the API defined the type of goals and tactics in Proof_type, and by the no-alias rule, this was the only one. But Proof_type was already implicitly deprecated, so that the API should have relied on Tacmach instead. --- plugins/ssrmatching/ssrmatching.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ssrmatching') diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index c2bf12cb6..1853bc35d 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -3,11 +3,11 @@ open API open Grammar_API +open Goal open Genarg open Tacexpr open Environ open Evd -open Proof_type open Term (** ******** Small Scale Reflection pattern matching facilities ************* *) -- cgit v1.2.3