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/ssrview.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ssr/ssrview.ml') diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 91e40f368..cc142e091 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -80,7 +80,7 @@ let interp_view ist si env sigma gv v rid = snd (view_with (if view_nbimps < 0 then [] else viewtab.(0))) -let with_view ist ~next si env (gl0 : (Proof_type.goal * tac_ctx) Evd.sigma) c name cl prune (conclude : EConstr.t -> EConstr.t -> tac_ctx tac_a) clr = +let with_view ist ~next si env (gl0 : (Goal.goal * tac_ctx) Evd.sigma) c name cl prune (conclude : EConstr.t -> EConstr.t -> tac_ctx tac_a) clr = let c2r ist x = { ist with lfun = Id.Map.add top_id (Value.of_constr x) ist.lfun } in let terminate (sigma, c') = -- cgit v1.2.3