diff options
| author | Hugo Herbelin | 2016-07-01 13:56:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-07-01 13:57:26 +0200 |
| commit | 622c663094717530bc767dacce44b39041b9a732 (patch) | |
| tree | 2d8049817ea5c80660bed69e3cf41da01ca093e1 | |
| parent | dae240f31d6de1d5b3737d6d0779e009f3d67fa2 (diff) | |
Fixing #4881 (synchronizing "Declare Implicit Tactic" with backtrack).
| -rw-r--r-- | proofs/pfedit.ml | 2 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 26 |
2 files changed, 23 insertions, 5 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 20cae84a49..d3162c54f2 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -215,7 +215,7 @@ let refine_by_tactic env sigma ty tac = (* Support for resolution of evars in tactic interpretation, including resolution by application of tactics *) -let implicit_tactic = ref None +let implicit_tactic = Summary.ref None ~name:"implicit-tactic" let declare_implicit_tactic tac = implicit_tactic := Some tac diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 15613c7ecc..92d0ac983d 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -525,11 +525,29 @@ VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF [ add_transitivity_lemma false t ] END +let cache_implicit_tactic (_,tac) = match tac with + | Some tac -> Pfedit.declare_implicit_tactic (Tacinterp.eval_tactic tac) + | None -> Pfedit.clear_implicit_tactic () + +let subst_implicit_tactic (subst,tac) = + Option.map (Tacsubst.subst_tactic subst) tac + +let inImplicitTactic : glob_tactic_expr option -> obj = + declare_object {(default_object "IMPLICIT-TACTIC") with + open_function = (fun i o -> if Int.equal i 1 then cache_implicit_tactic o); + cache_function = cache_implicit_tactic; + subst_function = subst_implicit_tactic; + classify_function = (fun o -> Dispose)} + +let declare_implicit_tactic tac = + Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac))) + +let clear_implicit_tactic () = + Lib.add_anonymous_leaf (inImplicitTactic None) + VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF -| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> - [ Pfedit.declare_implicit_tactic (Tacinterp.interp tac) ] -| [ "Clear" "Implicit" "Tactic" ] -> - [ Pfedit.clear_implicit_tactic () ] +| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> [ declare_implicit_tactic tac ] +| [ "Clear" "Implicit" "Tactic" ] -> [ clear_implicit_tactic () ] END |