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
*
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
*
Cleanup of comments.
aspiwack
2013-11-02
*
A whole new implemenation of the refine tactic.
aspiwack
2013-11-02
*
A newly introduced variable inside a named context is no longer α-renamed.
aspiwack
2013-11-02
*
Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.
aspiwack
2013-11-02
*
Bases tactics on an IO monad.
aspiwack
2013-11-02
*
Getting rid of Goal.here, and all the related exceptions and combinators.
aspiwack
2013-11-02
*
Uses Proofview.tclEXTEND more sparingly.
aspiwack
2013-11-02
*
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-11-02
*
Conv_orable made functional and part of pre_env
gareuselesinge
2013-10-31
*
Evar leak in "absurd" tactic.
ppedrot
2013-10-28
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
[next]