index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
lib
Commit message (
Expand
)
Author
Age
*
Adds a shelve tactic.
aspiwack
2013-11-02
*
Future: better doc + restore ~pure optimization
gareuselesinge
2013-10-31
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
Rtree : cleanup of the comparing code
letouzey
2013-10-24
*
Specializing hash functions for widely used types.
ppedrot
2013-10-24
*
Fix the semantic of the new List.remove_assoc_f
letouzey
2013-10-24
*
Ephemeron: add a function to run a collection cycle
gareuselesinge
2013-10-24
*
Turn many List.assoc into List.assoc_f
letouzey
2013-10-24
*
cList: a few alternative to hashtbl-based uniquize, distinct, subset
letouzey
2013-10-23
*
CList.factorize_left with a parametric equality
letouzey
2013-10-23
*
CList.prefix_of and CList.drop_prefix with a parametric equality
letouzey
2013-10-23
*
cList.index is now cList.index_f, same for index0
letouzey
2013-10-23
*
cList: set-as-list functions are now with an explicit comparison
letouzey
2013-10-23
*
Small optimizations in unification.
ppedrot
2013-10-23
*
Removing some generic equalities.
ppedrot
2013-10-22
*
Optimizing evar filters. It seems to cost quite a lot in unification,
ppedrot
2013-10-22
*
More efficient operations in CArray.
ppedrot
2013-10-22
*
New feedback message: SlaveStatus
gareuselesinge
2013-10-22
*
Future: ported to Ephemeron + exception enhancing
gareuselesinge
2013-10-18
*
Ephemeron: marshaling friendly keys
gareuselesinge
2013-10-18
*
Some more hand-written comparison functions to avoid polymorphic comparison.
xclerc
2013-10-14
*
Vcs: the gc method returns the set of nodes that were collected
gareuselesinge
2013-10-11
*
Dag: some comments on the concept of cluster
gareuselesinge
2013-10-11
*
Clib: fold_left_until added to CList
gareuselesinge
2013-10-10
*
cStack: make it just a Stack with some extra API
gareuselesinge
2013-10-07
*
Added a [modify] function to maps.
ppedrot
2013-10-06
*
STM: add options to disable fallbacks to ease regression testing
gareuselesinge
2013-10-03
*
STM: number of slaves passed by the command line
gareuselesinge
2013-10-03
*
typo
gareuselesinge
2013-10-01
*
CoqIDE protocol/serialization revised
gareuselesinge
2013-09-30
*
lib/cstack: various improvements
gareuselesinge
2013-09-30
*
lib/vcs: various improvements
gareuselesinge
2013-09-30
*
lib/dag: various improvements
gareuselesinge
2013-09-30
*
lib/future: computations that are Exn can be replaced
gareuselesinge
2013-09-30
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
CoqIDE: show number of proofs being checked in background
gareuselesinge
2013-09-12
*
Fix bug in CStack introduced by refactoring
gareuselesinge
2013-09-12
*
Moving Searchstack to CStack, and normalizing names a bit.
ppedrot
2013-09-06
*
* lib/Unicode:
regisgia
2013-09-02
*
recdef: restore old semantics (pre STM)
gareuselesinge
2013-08-30
*
safe Conv_oracle state for type checking
gareuselesinge
2013-08-30
*
Stm: if slave process dies badly go back to local lazy evaluation
gareuselesinge
2013-08-30
*
Removing some lone List.assoc & List.mem in lib.
ppedrot
2013-08-28
*
Removing association lists in Reductionops. Btw, defining the dual of the
ppedrot
2013-08-25
*
Added a more efficient way to recover the domain of a map.
ppedrot
2013-08-25
*
Misc changes around coqtop.ml :
letouzey
2013-08-22
*
More complete hashcons : lists (dirpath), arrays (constr)
letouzey
2013-08-22
*
Change in vo format : digest aren't Marshalled anymore
letouzey
2013-08-22
*
Universe counters on slaves are in sync with master
gareuselesinge
2013-08-20
[next]