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
*
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
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
Removing useless evar-related stuff.
ppedrot
2013-09-25
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Removing almost all new_untyped_evar, and a bunch of Evd.add.
ppedrot
2013-09-18
*
Partly replacing list-based access functions in Evd. This is still
ppedrot
2013-09-03
*
safe Conv_oracle state for type checking
gareuselesinge
2013-08-30
*
Replacing lists by sets in clear tactic.
ppedrot
2013-08-25
*
stm: (initial) support for -coq-slaves
gareuselesinge
2013-08-08
*
get rid of closures in global/proof state
gareuselesinge
2013-08-08
*
enhance marshallable option for freeze (minor TODO in safe_typing)
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Generalizing the use of maps instead of lists in the interpretation
ppedrot
2013-06-22
[next]