aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Expand)AuthorAge
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* Less ocaml warnings.Gravatar Hugo Herbelin2014-06-21
* Deprecate useless option -quality.Gravatar Guillaume Melquiond2014-06-13
* Deprecate useless option -unsafe.Gravatar Guillaume Melquiond2014-06-13
* Deprecate options -dont, -lazy, -force-load-proofs.Gravatar Guillaume Melquiond2014-06-13
* Compute the trace of a universe inconsistency only when explicitly requiredGravatar Pierre-Marie Pédrot2014-06-10
* Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofGravatar Pierre-Marie Pédrot2014-06-08
* Timeout implementation for Windows based on threads.Gravatar Pierre-Marie Pédrot2014-06-08
* Enforce a correct exception handling in declaration_hooksGravatar Enrico Tassi2014-06-08
* Moving a Thread.yield in check_interrupt.Gravatar Pierre-Marie Pédrot2014-06-07
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
* Declare: fix Future managementGravatar Enrico Tassi2014-05-16
* Future: better error messageGravatar Enrico Tassi2014-05-15
* Moving Dnet-related code to tactics/.Gravatar Pierre-Marie Pédrot2014-05-08
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing ml-doc.Gravatar Pierre-Marie Pédrot2014-05-01
* Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toGravatar Hugo Herbelin2014-04-28
* Adding a stm/ folder, as asked during last workgroup. It was essentially movingGravatar Pierre-Marie Pédrot2014-04-25
* Future: memory optimization when forcing a chained pure computationGravatar Enrico Tassi2014-04-25
* Adding a debug printer for futures.Gravatar Pierre-Marie Pédrot2014-04-25
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Have the feedback bus as a backend for dumping globs.Gravatar Carst Tankink2014-04-10
* Removing handshake from Spawn. It used marshalling, which is bad forGravatar Pierre-Marie Pédrot2014-04-09
* Change handling of loadpath and mlpath.Gravatar Guillaume Melquiond2014-04-06
* Slightly more efficient Array.smartmap & related.Gravatar Pierre-Marie Pédrot2014-03-20
* Stateid: export a Set moduleGravatar Enrico Tassi2014-03-13
* STM: move out a couple of submodulesGravatar Enrico Tassi2014-03-13
* Stm: smarter delegation policyGravatar Enrico Tassi2014-03-12
* Uses slashes for install and config directoriesGravatar Virgile Prevosto2014-03-06
* Canary testing absence of generic equality for KerNamesGravatar Pierre-Marie Pédrot2014-03-05
* Adding a canary library. This canary is imperfect. It allows serializationGravatar Pierre-Marie Pédrot2014-03-05
* Fixing compilation on OCaml 4.01.Gravatar Pierre-Marie Pédrot2014-03-05
* Fixing previous commit. Forgot to include some code.Gravatar Pierre-Marie Pédrot2014-03-05
* Added a new module HMap. It works (almost) like Map, except that it expectsGravatar Pierre-Marie Pédrot2014-03-05
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Adding a CSet module in Coq lib.Gravatar Pierre-Marie Pédrot2014-03-05
* Replacing arguments of Trie by a cancellable monoid.Gravatar Pierre-Marie Pédrot2014-03-03
* Fixing generic hashes and replacing them with proper ones.Gravatar Pierre-Marie Pédrot2014-03-03
* Set officially the minimal OCaml requirement to 3.12.1Gravatar Pierre Letouzey2014-03-02
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
* Fix output test-suite 'simpl tactic' -> 'reduction tactics'Gravatar Pierre Boutillier2014-02-28
* amending last commitGravatar Enrico Tassi2014-02-27
* better warningGravatar Enrico Tassi2014-02-27
* Tacinterp: more refactoring.Gravatar Arnaud Spiwack2014-02-27
* Tacinterp: refactoring using Monad.Gravatar Arnaud Spiwack2014-02-27
* Remove unsafe code (Obj.magic) in Tacinterp.Gravatar Arnaud Spiwack2014-02-27
* remoteCounter: backup/restoreGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Future: make ~greedy:true the default + new sink commodity APIGravatar Enrico Tassi2014-02-26