From ac9c5986b77bf4a783f2bd0ad571645694c960e1 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 16 Oct 2014 18:33:43 +0200
Subject: 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.
---
 plugins/decl_mode/decl_proof_instr.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins')

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 *)
-- 
cgit v1.2.3