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
*
Adding a "time" tactical for benchmarking purposes. In case the tactic
Hugo Herbelin
2014-07-13
*
An outdated comment + comment layout.
Arnaud Spiwack
2014-07-11
*
STM: let toploop plugins specify the flags for STM workers
Enrico Tassi
2014-07-11
*
STM: flag to turn off branch reopening
Enrico Tassi
2014-07-11
*
Feedback: LoadedFile + Goals
Enrico Tassi
2014-07-11
*
make the standard logging facility stm aware
Enrico Tassi
2014-07-11
*
option to always delegate futures to workers
Enrico Tassi
2014-07-10
*
more APIs in TQueue and CThread
Enrico Tassi
2014-07-10
*
check_for_interrupt: better (but slower) in threading mode
Enrico Tassi
2014-07-10
*
Revert "time tac" (committed by mistake).
Hugo Herbelin
2014-07-07
*
time tac
Hugo Herbelin
2014-07-07
*
Adding a coiterator to IStream.
Pierre-Marie Pédrot
2014-07-03
*
all coqide specific files moved into ide/
Enrico Tassi
2014-06-25
*
Less ocaml warnings.
Hugo Herbelin
2014-06-21
*
Deprecate useless option -quality.
Guillaume Melquiond
2014-06-13
*
Deprecate useless option -unsafe.
Guillaume Melquiond
2014-06-13
*
Deprecate options -dont, -lazy, -force-load-proofs.
Guillaume Melquiond
2014-06-13
*
Compute the trace of a universe inconsistency only when explicitly required
Pierre-Marie Pédrot
2014-06-10
*
Moving hook code from Future to Lemmas. This seemed to disrupt compilation of
Pierre-Marie Pédrot
2014-06-08
*
Timeout implementation for Windows based on threads.
Pierre-Marie Pédrot
2014-06-08
*
Enforce a correct exception handling in declaration_hooks
Enrico Tassi
2014-06-08
*
Moving a Thread.yield in check_interrupt.
Pierre-Marie Pédrot
2014-06-07
*
Adding a new Control file centralizing the control options of Coq.
Pierre-Marie Pédrot
2014-06-07
*
Declare: fix Future management
Enrico Tassi
2014-05-16
*
Future: better error message
Enrico Tassi
2014-05-15
*
Moving Dnet-related code to tactics/.
Pierre-Marie Pédrot
2014-05-08
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Fixing ml-doc.
Pierre-Marie Pédrot
2014-05-01
*
Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to
Hugo Herbelin
2014-04-28
*
Adding a stm/ folder, as asked during last workgroup. It was essentially moving
Pierre-Marie Pédrot
2014-04-25
*
Future: memory optimization when forcing a chained pure computation
Enrico Tassi
2014-04-25
*
Adding a debug printer for futures.
Pierre-Marie Pédrot
2014-04-25
*
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-04-23
*
Have the feedback bus as a backend for dumping globs.
Carst Tankink
2014-04-10
*
Removing handshake from Spawn. It used marshalling, which is bad for
Pierre-Marie Pédrot
2014-04-09
*
Change handling of loadpath and mlpath.
Guillaume Melquiond
2014-04-06
*
Slightly more efficient Array.smartmap & related.
Pierre-Marie Pédrot
2014-03-20
*
Stateid: export a Set module
Enrico Tassi
2014-03-13
*
STM: move out a couple of submodules
Enrico Tassi
2014-03-13
*
Stm: smarter delegation policy
Enrico Tassi
2014-03-12
*
Uses slashes for install and config directories
Virgile Prevosto
2014-03-06
*
Canary testing absence of generic equality for KerNames
Pierre-Marie Pédrot
2014-03-05
*
Adding a canary library. This canary is imperfect. It allows serialization
Pierre-Marie Pédrot
2014-03-05
*
Fixing compilation on OCaml 4.01.
Pierre-Marie Pédrot
2014-03-05
*
Fixing previous commit. Forgot to include some code.
Pierre-Marie Pédrot
2014-03-05
*
Added a new module HMap. It works (almost) like Map, except that it expects
Pierre-Marie Pédrot
2014-03-05
*
Remove some dead-code (thanks to ocaml warnings)
Pierre Letouzey
2014-03-05
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Adding a CSet module in Coq lib.
Pierre-Marie Pédrot
2014-03-05
*
Replacing arguments of Trie by a cancellable monoid.
Pierre-Marie Pédrot
2014-03-03
[next]