diff options
| author | Hugo Herbelin | 2015-10-24 17:53:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-30 10:34:04 +0100 |
| commit | 37ab457263e980aa49e681eceb3eb382ef8b36e3 (patch) | |
| tree | 633b55bb0f7cae26f44c4d8007062a37304e9c73 /tactics/tactics.mli | |
| parent | 74ba1999baa08a283c1743c22692bc575b40a0b9 (diff) | |
Moving apply_type to new proof engine.
Note that code depending on apply_type might now have to ensure that
typing constraints that were possibly generated by apply_type are now
taken into account in advance.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index c966adb801..098212048f 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -179,7 +179,7 @@ val revert : Id.t list -> unit Proofview.tactic (** {6 Resolution tactics. } *) -val apply_type : constr -> constr list -> tactic +val apply_type : constr -> constr list -> unit Proofview.tactic val bring_hyps : named_context -> unit Proofview.tactic val apply : constr -> unit Proofview.tactic |