diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-21 14:59:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-21 15:20:52 +0200 |
| commit | 1fbcea38dc9d995f7c6786b543675ba27970642e (patch) | |
| tree | c1d574f081038b403313daaed905521a5964603c /tactics/tactics.mli | |
| parent | 9a24bc736d5782b7b9c23ebd4cfcf5f5f99836eb (diff) | |
Removing unused parts of the Goal.sensitive monad.
Some legacy code remains to keep the newish refine tactic working, but
ultimately it should be removed. I did not manage to do it properly though,
i.e. without breaking the test-suite furthermore.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 238b95a46..e5ba7f14c 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -429,6 +429,9 @@ end module New : sig val refine : Evd.open_constr -> unit Proofview.tactic + (** DEPRECATED. Legacy refine tactic. You should not be using this code, as + it may be unsound to manipulate evar maps without care. Use the + [Proofview.Refine] module instead. *) open Proofview val exact_proof : Constrexpr.constr_expr -> unit tactic |