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/ltac | |
| 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/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 a0446bd6a0..124974b6e3 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 = |