index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
lib
Age
Commit message (
Expand
)
Author
2014-02-03
Tracking memory misallocation by trying to improve sharing.
Pierre-Marie Pédrot
2014-02-03
Allocation friendly map-handling functions in Dag.
Pierre-Marie Pédrot
2014-01-30
Relaunch all Unix.waitpid when they ended with EINTR
Pierre Letouzey
2014-01-30
CUnix: enriched (get_extension, sys_command, waitpid_non_intr) + cleaned
Pierre Letouzey
2014-01-30
CString: avoid redefining is_sub
Pierre Letouzey
2014-01-30
Remove useless Xml_utils
Pierre Letouzey
2014-01-30
clib.mllib: remove duplicated Flags entry
Pierre Letouzey
2014-01-30
STM + CoqIDE: stop_worker message and UI
Enrico Tassi
2014-01-30
Work around for bug in threads + blocking io streamlined
Enrico Tassi
2014-01-30
STM: tell the user if the master is recomputing states validated by workers
Enrico Tassi
2014-01-30
Fixing backtrace handling here and there.
Pierre-Marie Pédrot
2014-01-29
Adding a smartmap[i] operator to maps.
Pierre-Marie Pédrot
2014-01-26
CoqIDE: command line for extra coqtop "flags"
Enrico Tassi
2014-01-26
Spawn: managed processes
Enrico Tassi
2014-01-19
Adding a default object to generic argument registering mechanism.
Pierre-Marie Pédrot
2014-01-06
fix typo
Enrico Tassi
2014-01-05
Paral-ITP: cleanup of command line flags and more conservative default
Enrico Tassi
2014-01-04
.vi files: .vo files without proofs
Enrico Tassi
2014-01-04
Future: allow custom action when a delegated future is forced
Enrico Tassi
2014-01-04
Aux_file: cache information at compile time for later (re)use
Enrico Tassi
2013-12-24
CoqIDE: new feedback "incomplete" to signal partial Qed
Enrico Tassi
2013-12-24
Future: optional greedy chaining
Enrico Tassi
2013-12-19
Removing the useless pattern ident genarg.
Pierre-Marie Pédrot
2013-12-10
Fix CoqIDE on windows
Enrico Tassi
2013-12-01
Removing RefArgType generic argument.
Pierre-Marie Pédrot
2013-11-30
Getting rid of casted_open_constr. It was only used by the
Pierre-Marie Pédrot
2013-11-27
Old message Interp returns the state id so that one can BackTo it
Enrico Tassi
2013-11-27
New option --help-XML-protocol to document the XML procol used by -ideslave
Enrico Tassi
2013-11-27
First stab at retrocompatible INTERP message
Enrico Tassi
2013-11-26
Adding a generic Int.Map using persistent arrays.
Pierre-Marie Pédrot
2013-11-24
Adding fold_left / fold_right function to maps.
Pierre-Marie Pédrot
2013-11-24
Hardening the reading function of vo files.
Pierre-Marie Pédrot
2013-11-24
Tweaking arity & allocation of some basic functions.
Pierre-Marie Pédrot
2013-11-22
Using hashes instead of strings in dynamic tags. In case of collision, an
Pierre-Marie Pédrot
2013-11-16
Better implementation for stores.
ppedrot
2013-11-13
Adding an unsafe mapping function to maps.
ppedrot
2013-11-08
Useless array manipulation in Rtrees.
ppedrot
2013-11-08
Do not compute formatter UTF8 length at creation time.
ppedrot
2013-11-07
Partial application hunt.
ppedrot
2013-11-06
better IStream.concat
ppedrot
2013-11-04
Adding closure-preventing functions in CArray. These functions are all
ppedrot
2013-11-04
Allocation friendly version of Util.iterate.
ppedrot
2013-11-04
Added an update function in CMap. It has the same signature as Map.add, but
ppedrot
2013-11-04
Manual coding of Int.Map.find. We use unsafe features, but this function
ppedrot
2013-11-02
Adds a tactic give_up.
aspiwack
2013-11-02
Adds a shelve tactic.
aspiwack
2013-10-31
Future: better doc + restore ~pure optimization
gareuselesinge
2013-10-24
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
[next]