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