diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-20 04:16:15 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-25 11:05:51 +0100 |
| commit | b508e2b745be0c38c18f2b8874adf8550bbe6d96 (patch) | |
| tree | 0a328549f514ea08b9ad4919be24342c95b57376 /tactics/tactics.mli | |
| parent | df9d69f3ccf3e5600919a21112afda00b463fbc5 (diff) | |
Moving specialize to Proofview.tactic.
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 f5695ff06..c966adb80 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -170,7 +170,7 @@ val unfold_body : Id.t -> tactic val keep : Id.t list -> unit Proofview.tactic val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic -val specialize : constr with_bindings -> tactic +val specialize : constr with_bindings -> unit Proofview.tactic val move_hyp : Id.t -> Id.t move_location -> tactic val rename_hyp : (Id.t * Id.t) list -> unit Proofview.tactic |