diff options
| -rw-r--r-- | proofs/goal.ml | 15 | ||||
| -rw-r--r-- | proofs/goal.mli | 10 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 7 |
3 files changed, 13 insertions, 19 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 43d7b3579..c660f403f 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -232,27 +232,20 @@ module Refinable = struct many things to go wrong. *) handle := fusion delta_list !handle - (* [constr_of_raw] is a pretyping function. The [check_type] argument - asks whether the term should have the same type as the conclusion. - [resolve_classes] is a flag on pretyping functions which, if set to true, - calls the typeclass resolver. + (* [constr_of_raw h tycon flags] is a pretyping function. + The [tycon] argument allows to put a type constraint on the returned term. + The [flags] argument is passed to the pretyper. 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.*) (* 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 lvar rawc = (); fun env rdefs gl info -> + let constr_of_raw handle tycon flags 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 - proof-to-be *) - let tycon = if check_type then Pretyping.OfType (Evd.evar_concl info) else Pretyping.WithoutTypeConstraint in (* call to [understand_tcc_evars] returns a constr with undefined evars these evars will be our new goals *) - let flags = - if resolve_classes then Pretyping.all_no_fail_flags - else Pretyping.no_classes_no_fail_inference_flags in let (sigma, open_constr) = Pretyping.understand_ltac flags !rdefs env lvar tycon rawc in diff --git a/proofs/goal.mli b/proofs/goal.mli index 013b3199a..db864b273 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -86,14 +86,14 @@ module Refinable : sig val resolve_typeclasses : ?filter:Typeclasses.evar_filter -> ?split:bool -> ?fail:bool -> unit -> unit sensitive - (* [constr_of_raw h check_type resolve_classes] is a pretyping function. - The [check_type] argument asks whether the term should have the same - type as the conclusion. [resolve_classes] is a flag on pretyping functions - which, if set to true, calls the typeclass resolver. + (* [constr_of_raw h tycon flags] is a pretyping function. + The [tycon] argument allows to put a type constraint on the returned term. + The [flags] argument is passed to the pretyper. 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 -> Pretyping.ltac_var_map -> + val constr_of_raw : handle -> Pretyping.typing_constraint -> + Pretyping.inference_flags -> Pretyping.ltac_var_map -> Glob_term.glob_constr -> Term.constr sensitive (* [constr_of_open_constr h check_type] transforms an open constr into a diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 031cbc7c5..a1e57fd3c 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -322,8 +322,6 @@ END (* Refine *) -let refine_tac = Tactics.New.refine - let refine_red_flags = Genredexpr.Lazy { Genredexpr.rBeta=true; @@ -341,7 +339,10 @@ let refine_tac (ist, c) = 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 + Goal.bind Goal.concl (fun concl -> + let flags = Pretyping.all_no_fail_flags in + let tycon = Pretyping.OfType concl in + Goal.Refinable.constr_of_raw h tycon flags vars c) end in Proofview.Goal.lift c >>= fun c -> Proofview.tclSENSITIVE (Goal.refine c) <*> |