diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 29 |
1 files changed, 24 insertions, 5 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index cab74968..15613c7e 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -21,6 +21,7 @@ open Util open Evd open Equality open Misctypes +open Proofview.Notations DECLARE PLUGIN "extratactics" @@ -264,7 +265,7 @@ TACTIC EXTEND rewrite_star let add_rewrite_hint bases ort t lcsr = let env = Global.env() in let sigma = Evd.from_env env in - let poly = Flags.is_universe_polymorphism () in + let poly = Flags.use_polymorphic_flag () in let f ce = let c, ctx = Constrintern.interp_constr env sigma ce in let ctx = @@ -344,7 +345,7 @@ END (**********************************************************************) (* Refine *) -let refine_tac {Glob_term.closure=closure;term=term} = +let refine_tac simple {Glob_term.closure=closure;term=term} = Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in @@ -356,11 +357,19 @@ let refine_tac {Glob_term.closure=closure;term=term} = Pretyping.ltac_idents = closure.Glob_term.idents; } in let update evd = Pretyping.understand_ltac flags env evd lvar tycon term in - Tactics.New.refine ~unsafe:false update + let refine = Proofview.Refine.refine ~unsafe:false update in + if simple then refine + else refine <*> + Tactics.New.reduce_after_refine <*> + Proofview.shelve_unifiable end TACTIC EXTEND refine - [ "refine" uconstr(c) ] -> [ refine_tac c ] +| [ "refine" uconstr(c) ] -> [ refine_tac false c ] +END + +TACTIC EXTEND simple_refine +| [ "simple" "refine" uconstr(c) ] -> [ refine_tac true c ] END (**********************************************************************) @@ -864,6 +873,16 @@ TACTIC EXTEND shelve_unifiable [ Proofview.shelve_unifiable ] END +(* Unshelves the goal shelved by the tactic. *) +TACTIC EXTEND unshelve +| [ "unshelve" tactic1(t) ] -> + [ + Proofview.with_shelf (Tacinterp.eval_tactic t) >>= fun (gls, ()) -> + Proofview.Unsafe.tclGETGOALS >>= fun ogls -> + Proofview.Unsafe.tclSETGOALS (gls @ ogls) + ] +END + (* Command to add every unshelved variables to the focus *) VERNAC COMMAND EXTEND Unshelve [ "Unshelve" ] |