diff options
| -rw-r--r-- | proofs/goal.ml | 7 | ||||
| -rw-r--r-- | proofs/goal.mli | 4 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 16 |
3 files changed, 16 insertions, 11 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index ae42acf18..43d7b3579 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -242,7 +242,7 @@ module Refinable = struct (* spiwack: it is not entirely satisfactory to have this function here. Plus it is a bit hackish. However it does not seem possible to move it out until pretyping is defined as some proof procedure. *) - let constr_of_raw handle check_type resolve_classes rawc = (); fun env rdefs gl info -> + let constr_of_raw handle check_type resolve_classes lvar rawc = (); fun env rdefs gl info -> (* We need to keep trace of what [rdefs] was originally*) let init_defs = !rdefs in (* if [check_type] is true, then creates a type constraint for the @@ -253,9 +253,10 @@ module Refinable = struct let flags = if resolve_classes then Pretyping.all_no_fail_flags else Pretyping.no_classes_no_fail_inference_flags in - let open_constr = - Pretyping.understand_tcc_evars ~flags rdefs env ~expected_type:tycon rawc + let (sigma, open_constr) = + Pretyping.understand_ltac flags !rdefs env lvar tycon rawc in + let () = rdefs := sigma in let () = update_handle handle init_defs !rdefs in open_constr diff --git a/proofs/goal.mli b/proofs/goal.mli index 1f04ce8c1..013b3199a 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -93,8 +93,8 @@ module Refinable : sig The principal argument is a [glob_constr] which is then pretyped in the context of a term, the remaining evars are registered to the handle. It is the main component of the toplevel refine tactic.*) - val constr_of_raw : - handle -> bool -> bool -> Glob_term.glob_constr -> Term.constr sensitive + val constr_of_raw : handle -> bool -> bool -> Pretyping.ltac_var_map -> + Glob_term.glob_constr -> Term.constr sensitive (* [constr_of_open_constr h check_type] transforms an open constr into a goal-sensitive constr, adding the undefined variables to the set of subgoals. diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 18326435c..2e753e0cc 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -336,12 +336,16 @@ let refine_red_flags = let refine_locs = { Locus.onhyps=None; concl_occs=Locus.AllOccurrences } let refine_tac (ist, c) = - let c = Goal.Refinable.make begin fun h -> - Goal.Refinable.constr_of_raw h true true c - end in - Proofview.Goal.lift c >>= fun c -> - Proofview.tclSENSITIVE (Goal.refine c) <*> - Proofview.V82.tactic (reduce refine_red_flags refine_locs) + Proofview.Goal.enter (fun gl -> + let env = Proofview.Goal.env gl in + let constrvars = Tacinterp.extract_ltac_constr_values ist env in + let vars = (constrvars, ist.Geninterp.lfun) in + let c = Goal.Refinable.make begin fun h -> + Goal.Refinable.constr_of_raw h true true vars c + end in + Proofview.Goal.lift c >>= fun c -> + Proofview.tclSENSITIVE (Goal.refine c) <*> + Proofview.V82.tactic (reduce refine_red_flags refine_locs)) TACTIC EXTEND refine [ "refine" glob(c) ] -> [ refine_tac c ] |