aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2013-11-19Optimization: in case of empty substitution, merging is trivial.Pierre-Marie Pédrot
2013-11-16Slightly faster version of merging substitutions in TacticMatching.ppedrot
2013-11-14Changes the semantics of Ltac's non-lazy pattern matching in presence of mult...aspiwack
2013-11-14Implementation of Ltac's match and match goal fully based on IStream.aspiwack
2013-11-14Remove some dead code in tacinterp.aspiwack
2013-11-12Do not print tactic notation names at each interpretation step.ppedrot
2013-11-10Centralizing the Ltac-defining functions in Tacenv.ppedrot
2013-11-10Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-09Revert the previous commit. It broke Coq compilation.ppedrot
2013-11-09Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-08Porting Tactics.assumption to the new engine.ppedrot
2013-11-04Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was sol...aspiwack
2013-11-04Fix ltac's progress tactical: requires progress in each goal.aspiwack
2013-11-04Fix the tactical ; [ … ] : the "incorrect number of goal" error was not cau...aspiwack
2013-11-04Fix change: nf_evar prior to tactic interpretation.aspiwack
2013-11-04Allowing proofs starting with a non-empty evarmap.ppedrot
2013-11-02Fixing CAMLP4 compilation.ppedrot
2013-11-02Fix set: nf_evar prior to tactic interpretation.aspiwack
2013-11-02Plug back infoH.aspiwack
2013-11-02Plugs back external tactics.aspiwack
2013-11-02Fix the log of debug auto.aspiwack
2013-11-02Update comments.aspiwack
2013-11-02Doc: solve the bad interaction between Declare Implicit Tactic and refine.aspiwack
2013-11-02The repeat tactic now honors failure levels in ltac.aspiwack
2013-11-02Fix destruct: nf_evar prior to tactic interpretation.aspiwack
2013-11-02Tacticals.New.tclWITHHOLES: clean up.aspiwack
2013-11-02Refine now does iota reduction in addition to beta.aspiwack
2013-11-02Refine: Tactics.New.refine does beta-reduction.aspiwack
2013-11-02Adds a tactic give_up.aspiwack
2013-11-02A tactic shelve_unifiable.aspiwack
2013-11-02Made multiple-goal tactic work after all: .aspiwack
2013-11-02Make multiple-goal tactics possible after a tclTHEN.aspiwack
2013-11-02Adds a shelve tactic.aspiwack
2013-11-02Adds an experimental exactly_once tactical.aspiwack
2013-11-02Made Proofview.Goal.hyps a named_context.aspiwack
2013-11-02Refine does beta-reductions.aspiwack
2013-11-02Adds a tactical once.aspiwack
2013-11-02Corrects the semantics of the "+" tactical.aspiwack
2013-11-02Less use of the list-based interface for goal-bound tactics.aspiwack
2013-11-02Tachmach.New is now in Proofview.Goal.enter style.aspiwack
2013-11-02More Proofview.Goal.enter.aspiwack
2013-11-02Added the tactical "tac1 + tac2".aspiwack
2013-11-02Try to remove intermediate allocations when dealing with goal-specific tactics.aspiwack
2013-11-02Various rewriting, mostly for speed purposes.aspiwack
2013-11-02Fix behaviour of the refine tactic with respect to evars in types.aspiwack
2013-11-02Makes the Ltac debugger usable again.aspiwack
2013-11-02Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...aspiwack
2013-11-02Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).aspiwack
2013-11-02Clean up a warning.aspiwack
2013-11-02The tactic [admit] exits with the "unsafe" status.aspiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 17:46:39 +0000