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/ssr/ssrprinters.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ssr/ssrprinters.mli') diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 9207b9e43..8da9bc72b 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -12,7 +12,7 @@ open API open Ssrast val pp_term : - Proof_type.goal Evd.sigma -> EConstr.constr -> Pp.std_ppcmds + Goal.goal Evd.sigma -> EConstr.constr -> Pp.std_ppcmds val pr_spc : unit -> Pp.std_ppcmds val pr_bar : unit -> Pp.std_ppcmds -- cgit v1.2.3