diff options
Diffstat (limited to 'plugins/funind/functional_principles_proofs.mli')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 5bb288678d..64fbfaeedf 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -1,10 +1,9 @@ -open API open Names val prove_princ_for_struct : Evd.evar_map ref -> bool -> - int -> Constant.t array -> EConstr.constr array -> int -> Proof_type.tactic + int -> Constant.t array -> EConstr.constr array -> int -> Tacmach.tactic val prove_principle_for_gen : @@ -14,7 +13,7 @@ val prove_principle_for_gen : int -> (* the number of recursive argument *) EConstr.types -> (* the type of the recursive argument *) EConstr.constr -> (* the wf relation used to prove the function *) - Proof_type.tactic + Tacmach.tactic (* val is_pte : rel_declaration -> bool *) |