diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 18:33:43 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-22 07:31:44 +0200 |
| commit | ac9c5986b77bf4a783f2bd0ad571645694c960e1 (patch) | |
| tree | 80fe413054d56e52a75c6a061f174bd532311831 /tactics/extratactics.ml4 | |
| parent | 81b812c0512fb61342e3f43ebc29bf843a079321 (diff) | |
Remove the deprecated open-constr based refine.
That is [Tactics.New.refine]. Replaced it with a wrapper around the primitive refine [Proofview.Refine.refine], but with extra reductions on the resulting goals.
There was two used of this refine: one in the declarative mode, and one in type classes. The porting of the latter is likely to have introduced bugs.
Factored code with Ltac's refine in Extratactics.
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 15 |
1 files changed, 1 insertions, 14 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index e0995096f..71d766e12 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -349,18 +349,6 @@ END (**********************************************************************) (* Refine *) - -let refine_red_flags = - Genredexpr.Lazy { - Genredexpr.rBeta=true; - rIota=true; - rZeta=false; - rDelta=false; - rConst=[]; - } - -let refine_locs = { Locus.onhyps=None; concl_occs=Locus.AllOccurrences } - let refine_tac {Glob_term.closure=closure;term=term} = Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in @@ -373,8 +361,7 @@ let refine_tac {Glob_term.closure=closure;term=term} = Pretyping.ltac_idents = closure.Glob_term.idents; } in let update evd = Pretyping.understand_ltac flags env evd lvar tycon term in - Proofview.Refine.refine ~unsafe:false update <*> - Proofview.V82.tactic (reduce refine_red_flags refine_locs) + Tactics.New.refine ~unsafe:false update end TACTIC EXTEND refine |