diff options
| author | Arnaud Spiwack | 2014-10-16 18:33:43 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-22 07:31:44 +0200 |
| commit | ac9c5986b77bf4a783f2bd0ad571645694c960e1 (patch) | |
| tree | 80fe413054d56e52a75c6a061f174bd532311831 /proofs/proof.mli | |
| 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 'proofs/proof.mli')
0 files changed, 0 insertions, 0 deletions