aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/functional_principles_proofs.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
-rw-r--r--plugins/funind/functional_principles_proofs.ml3
1 files changed, 1 insertions, 2 deletions
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
}