diff options
| author | Pierre-Marie Pédrot | 2018-08-13 19:47:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-08-13 20:40:23 +0200 |
| commit | 5fcbb0eb7b624ee18b817e7fd1b3b0d2fbc9bd35 (patch) | |
| tree | 7072e91deaa91a9a37385d20f7cfc5d4c49f6cb6 /plugins/ssr | |
| parent | 18b662aa306c58d46292bdf79a2929c91d7d96fd (diff) | |
Less crazy implementation of the "pose" family of tactics.
The previous implementation was calling a lot of useless unification
even though the net effect of the tactic was simply to add a binding to
the environment.
Interestingly the base tactic was used in several higher level tactics,
including evar and ssreflect pose.
Part of the fix for #8245.
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 4 | ||||
| -rw-r--r-- | plugins/ssr/ssrtacticals.ml | 4 |
2 files changed, 2 insertions, 6 deletions
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index e367cd32d6..f67cf20e49 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -25,9 +25,7 @@ module RelDecl = Context.Rel.Declaration (** 8. Forward chaining tactics (pose, set, have, suffice, wlog) *) (** Defined identifier *) - -let settac id c = Tactics.letin_tac None (Name id) c None -let posetac id cl = Proofview.V82.of_tactic (settac id cl Locusops.nowhere) +let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl) let ssrposetac (id, (_, t)) gl = let ist, t = diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 83581f3416..f12f9fac0f 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -14,7 +14,6 @@ open Names open Constr open Termops open Tacmach -open Locusops open Ssrast open Ssrcommon @@ -82,8 +81,7 @@ let pf_clauseids gl gens clseq = let hidden_clseq = function InHyps | InHypsSeq | InAllHyps -> true | _ -> false -let settac id c = Tactics.letin_tac None (Name id) c None -let posetac id cl = Proofview.V82.of_tactic (settac id cl nowhere) +let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl) let hidetacs clseq idhide cl0 = if not (hidden_clseq clseq) then [] else |