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/ltac | |
| 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/ltac')
| -rw-r--r-- | plugins/ltac/evar_tactics.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 14 |
2 files changed, 9 insertions, 7 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 84f13d2131..73490a2dfd 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -94,7 +94,7 @@ let let_evar name typ = in let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Namegen.IntroFresh id) typ in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (Tactics.letin_tac None (Name.Name id) evar None Locusops.nowhere) + (Tactics.pose_tac (Name.Name id) evar) end let hget_evar n = diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index f4313a8fa3..71da6c7667 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1664,16 +1664,18 @@ and interp_atomic ist tac : unit Proofview.tactic = (* We try to fully-typecheck the term *) let flags = open_constr_use_classes_flags () in let (sigma,c_interp) = interp_open_constr ~flags ist env sigma c in - let let_tac b na c cl eqpat = - let id = Option.default (make IntroAnonymous) eqpat in - let with_eq = if b then None else Some (true,id) in - Tactics.letin_tac with_eq na c None cl - in let na = interp_name ist env sigma na in + let let_tac = + if b then Tactics.pose_tac na c_interp + else + let id = Option.default (make IntroAnonymous) eqpat in + let with_eq = Some (true, id) in + Tactics.letin_tac with_eq na c_interp None Locusops.nowhere + in Tacticals.New.tclWITHHOLES ev (name_atomic ~env (TacLetTac(ev,na,c_interp,clp,b,eqpat)) - (let_tac b na c_interp clp eqpat)) sigma + let_tac) sigma else (* We try to keep the pattern structure as much as possible *) let let_pat_tac b na c cl eqpat = |