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 /proofs/proofview.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 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 288a46cb7..4472bbcb7 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -394,10 +394,6 @@ module Goal : sig val env : 'a t -> Environ.env val sigma : 'a t -> Evd.evar_map - (* [lift_sensitive s k] applies [s] in each goal independently - raising result [a] then continues with [k a]. *) - val lift : 'a Goal.sensitive -> ('a->unit tactic) -> unit tactic - (* [enter t] execute the goal-dependent tactic [t] in each goal independently. In particular [t] need not backtrack the same way in each goal. *) |