diff options
| -rw-r--r-- | tactics/extratactics.ml4 | 14 | ||||
| -rw-r--r-- | tactics/tactics.ml | 9 |
2 files changed, 10 insertions, 13 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index e45c2170a..e6578ce52 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -321,23 +321,13 @@ END (**********************************************************************) (* Refine *) -open Genredexpr -open Locus -let refine c = - Proofview.tclTHEN - (Tactics.New.refine c) - (Proofview.V82.tactic (Tactics.reduce - (Lazy {rBeta=true;rIota=false;rZeta=false;rDelta=false;rConst=[]}) - {onhyps=None; concl_occs=AllOccurrences } - )) +let refine_tac = Tactics.New.refine TACTIC EXTEND refine - [ "refine" casted_open_constr(c) ] -> [ refine c ] + [ "refine" casted_open_constr(c) ] -> [ refine_tac c ] END -let refine_tac = Tactics.New.refine - (**********************************************************************) (* Inversion lemmas (Leminv) *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2d1ba7756..c933ec44e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3870,11 +3870,18 @@ module New = struct let exact_proof c = Proofview.V82.tactic (exact_proof c) + open Genredexpr + open Locus + let refine c = let c = Goal.Refinable.make begin fun h -> Goal.Refinable.constr_of_open_constr h true c end in Proofview.Goal.lift c >>= fun c -> - Proofview.tclSENSITIVE (Goal.refine c) + Proofview.tclSENSITIVE (Goal.refine c) <*> + Proofview.V82.tactic (reduce + (Lazy {rBeta=true;rIota=false;rZeta=false;rDelta=false;rConst=[]}) + {onhyps=None; concl_occs=AllOccurrences } + ) end |