diff options
| author | Maxime Dénès | 2017-06-20 08:09:00 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-20 08:09:00 +0200 |
| commit | 25cd7acea0df79fcc07274e429c9839de1246611 (patch) | |
| tree | 1ee95df49ec9ea7152afed41df425ea4e4760736 /plugins/funind/functional_principles_proofs.mli | |
| parent | c7ac5dc8036623a02ab4ad6d11469e040e78c004 (diff) | |
| parent | 0437339ccac602d692b5b8c071b77ac756805520 (diff) | |
Merge PR#803: Clean ssr
Diffstat (limited to 'plugins/funind/functional_principles_proofs.mli')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 5bb288678d..d03fc475e0 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -4,7 +4,7 @@ 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 +14,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 *) |