diff options
| author | Pierre-Marie Pédrot | 2014-08-21 14:59:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-21 15:20:52 +0200 |
| commit | 1fbcea38dc9d995f7c6786b543675ba27970642e (patch) | |
| tree | c1d574f081038b403313daaed905521a5964603c /tactics | |
| 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')
| -rw-r--r-- | tactics/tactics.ml | 8 | ||||
| -rw-r--r-- | tactics/tactics.mli | 3 |
2 files changed, 6 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 62c3a8fc16..7a8bb36b9a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4050,11 +4050,9 @@ module New = struct open Locus let refine c = - let c = Goal.Refinable.make begin fun h -> - Goal.Refinable.constr_of_open_constr h true c - end in - Proofview.Goal.lift c begin fun c -> - Proofview.tclSENSITIVE (Goal.refine c) <*> + Proofview.Goal.enter begin fun gl -> + let pf = Goal.refine_open_constr c in + Proofview.tclSENSITIVE pf <*> Proofview.V82.tactic (reduce (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]}) {onhyps=None; concl_occs=AllOccurrences } diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 238b95a467..e5ba7f14ce 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 |