index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
Commit message (
Expand
)
Author
Age
*
Adds a tactic give_up.
aspiwack
2013-11-02
*
A tactic shelve_unifiable.
aspiwack
2013-11-02
*
Corrects a bug on Proofview.Goal.enter whereby sigmas were captured and used ...
aspiwack
2013-11-02
*
Adds a shelve tactic.
aspiwack
2013-11-02
*
bootstrap/Monad.v: implements the writer monad in continuation passing style.
aspiwack
2013-11-02
*
bootstrap/Monad.v: implements the environment monad in continuation passing s...
aspiwack
2013-11-02
*
Adds an experimental exactly_once tactical.
aspiwack
2013-11-02
*
Normalise goals with respect to evars in the new tactics.
aspiwack
2013-11-02
*
Made Proofview.Goal.hyps a named_context.
aspiwack
2013-11-02
*
A dedicated view type for Proofview_gen.split.
aspiwack
2013-11-02
*
Adds a tactical once.
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
*
A better version of Goal.advance.
aspiwack
2013-11-02
*
bootstrap/Monads.v: A more efficient split.
aspiwack
2013-11-02
*
State monad implemented in CPS.
aspiwack
2013-11-02
*
A more principled split.
aspiwack
2013-11-02
*
Set an extraction flag for inling let-s in Monad.v.
aspiwack
2013-11-02
*
More optimisations of partial applications.
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
*
Optimisation of partial applications in the tactic monad.
aspiwack
2013-11-02
*
Makes the Ltac debugger usable again.
aspiwack
2013-11-02
*
New option Default Goal Selector.
aspiwack
2013-11-02
*
Adds a new goal selector "all:".
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
*
The tactic [admit] exits with the "unsafe" status.
aspiwack
2013-11-02
*
Cleanup of comments.
aspiwack
2013-11-02
*
Small change to the IO monad interface: [val ref : 'a -> 'a ref t]
aspiwack
2013-11-02
*
A whole new implemenation of the refine tactic.
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
*
Future: better doc + restore ~pure optimization
gareuselesinge
2013-10-31
*
Conv_orable made functional and part of pre_env
gareuselesinge
2013-10-31
*
Do not generate useless argument arrays in whd_* functions.
ppedrot
2013-10-29
*
Useless array to list conversions in proof/logic.ml.
ppedrot
2013-10-28
*
Abstracting evar filter away. The API is not perfect, but better than nothing.
ppedrot
2013-10-27
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
cList: a few alternative to hashtbl-based uniquize, distinct, subset
letouzey
2013-10-23
*
cList: set-as-list functions are now with an explicit comparison
letouzey
2013-10-23
*
proof modes: use ephemerons to represent them in proof state
gareuselesinge
2013-10-18
*
declaration_hooks use Ephemeron
gareuselesinge
2013-10-18
*
Future: ported to Ephemeron + exception enhancing
gareuselesinge
2013-10-18
*
Removing dubious use of evarmap manipulating functions in printing
ppedrot
2013-10-05
*
Moving side effects into evar_map. There was no reason to keep another
ppedrot
2013-10-05
[next]