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/funind/functional_principles_proofs.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'plugins/funind/functional_principles_proofs.ml') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ef894b239..ba46f78aa 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -10,7 +10,6 @@ open Names open Pp open Tacmach open Termops -open Proof_type open Tacticals open Tactics open Indfun_common @@ -106,7 +105,7 @@ let make_refl_eq constructor type_of_t t = type pte_info = { - proving_tac : (Id.t list -> Proof_type.tactic); + proving_tac : (Id.t list -> Tacmach.tactic); is_valid : constr -> bool } -- cgit v1.2.3