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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 470dc9d9cc..9d64efdeda 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1270,17 +1270,17 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = | End_patt (_,_) , _ :: _ -> anomaly ~label:"execute_cases " (Pp.str "End of branch with garbage left") -let understand_my_constr c gls = - let env = pf_env gls in +let understand_my_constr env sigma c concl = + let env = env in let rawc = Detyping.detype false [] env Evd.empty c in let rec frob = function | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,Misctypes.IntroAnonymous,None) | rc -> map_glob_constr frob rc in - Pretyping.understand_tcc env (sig_sig gls) ~expected_type:(Pretyping.OfType (pf_concl gls)) (frob rawc) + Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc) let my_refine c gls = - let oc = understand_my_constr c gls in + let oc sigma = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in Proofview.V82.of_tactic (Tactics.New.refine oc) gls (* end focus/claim *) |