diff options
| author | Enrico Tassi | 2018-09-19 18:20:10 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-09-19 18:20:10 +0200 |
| commit | 3781e50331d563b47f1ea1ce1773a71db68fdb2a (patch) | |
| tree | 9314761d99f9326948d812661c6f563d6c98c2a6 /plugins/ssr | |
| parent | 007c084e3935eae639bb83c9dd9deefc1363d71d (diff) | |
| parent | 5fcbb0eb7b624ee18b817e7fd1b3b0d2fbc9bd35 (diff) | |
Merge PR #8246: Implementing an internal basic version of the "pose" tactic independent of the multi-usage internal "letin_tac"
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 |