diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-17 11:02:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-17 11:06:14 +0200 |
| commit | 43343c1f79d9f373104ae5174baf41e2257e2b8d (patch) | |
| tree | 7ac3a1ec228702fd8bf81c828e3d3e1c8f0ebc3c /tactics/tactics.mli | |
| parent | cddddce068bc0482f62ffab8e412732a307b90bb (diff) | |
Removing the old refine tactic from the Tactics module.
It is indeed confusing, as it has little to do with the proper refine defined
in the New submodule. Legacy code relying on it should call the Logic or
Tacmach modules instead.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 24aca2a68..df41951c3 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -30,7 +30,6 @@ val is_quantified_hypothesis : Id.t -> ([`NF],'b) Proofview.Goal.t -> bool (** {6 Primitive tactics. } *) val introduction : ?check:bool -> Id.t -> unit Proofview.tactic -val refine : constr -> tactic val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic val convert_hyp : ?check:bool -> Context.Named.Declaration.t -> unit Proofview.tactic val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic |