aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fix compilation with ocaml 4.0.0Gravatar Enrico Tassi2014-12-17
* checker: Change in library on disk values, now using context_sets instead ofGravatar Matthieu Sozeau2014-12-17
* Ensuring the good invariants of hashcons table generation in the API.Gravatar Pierre-Marie Pédrot2014-12-17
* Fix (actually, properly implement :) hashconsing of projections,Gravatar Matthieu Sozeau2014-12-17
* Fixing bug #3796.Gravatar Pierre-Marie Pédrot2014-12-17
* Fixing Makefile so that it puts the -thread flag on the right place.Gravatar Pierre-Marie Pédrot2014-12-17
* Update checker/values and cic due to changes in case_info and record_body.Gravatar Matthieu Sozeau2014-12-17
* Future: blocking by defaultGravatar Enrico Tassi2014-12-17
* STM: resilient on errors in non delegated proofsGravatar Enrico Tassi2014-12-17
* CoqIDE: cleanup jobs window on worker deathGravatar Enrico Tassi2014-12-17
* STM: rename and simplify flagsGravatar Enrico Tassi2014-12-17
* STM: simplify state managementGravatar Enrico Tassi2014-12-17
* AsyncTaskQueue: simpler model (no parking area, continuation tasks)Gravatar Enrico Tassi2014-12-17
* WorkerPool: simpler fuctor and no more parking areaGravatar Enrico Tassi2014-12-17
* TQueue: a way to unblock threads begin destroyed waiting on popGravatar Enrico Tassi2014-12-17
* Spawn: fix request of Gc statisticsGravatar Enrico Tassi2014-12-17
* CThread: use a different type for thread friendly in_channelsGravatar Enrico Tassi2014-12-17
* Summary: more surgery functionsGravatar Enrico Tassi2014-12-17
* Global: export the name of the summary entryGravatar Enrico Tassi2014-12-17
* Dyn: add API to check of two Dyn.t are ==Gravatar Enrico Tassi2014-12-17
* Arguments: warn only if no option is given (Close 3860)Gravatar Enrico Tassi2014-12-17
* CoqIDE: better messagesGravatar Enrico Tassi2014-12-17
* Revert and correctly fix "#4843 part 2 : The .cmxs files for plugins must hav...Gravatar Pierre Boutillier2014-12-17
* #3828 is solved.Gravatar Hugo Herbelin2014-12-16
* Moving #2447 (congruence) to fixed.Gravatar Hugo Herbelin2014-12-16
* In CHANGES, alerting about stronger check on notation level modifiers.Gravatar Hugo Herbelin2014-12-16
* More printers for ltac signatures.Gravatar Hugo Herbelin2014-12-16
* Test for #3654.Gravatar Hugo Herbelin2014-12-16
* fix bug #2447 in congruenceGravatar Pierre Corbineau2014-12-16
|\
* | fix bug #2447 in congruenceGravatar Pierre Corbineau2014-12-16
| * Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
| * msg_info now puts infomsg tag in emacs mode.Gravatar Pierre Courtieu2014-12-16
| * Proper thread-safe implementation for Exninfo.Gravatar Pierre-Marie Pédrot2014-12-16
| * Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
| * Error messages of Searchxxx are coherent with goal selector.Gravatar Pierre Courtieu2014-12-16
|/
* Fix for #3154: use CUnix.sys_command to call native compiler.Gravatar Maxime Dénès2014-12-16
* Changed bullet informations to warning for better display in PG.Gravatar Pierre Courtieu2014-12-15
* Adapted test file for About.Gravatar Pierre Courtieu2014-12-15
* Tentatively starting to use heuristics for evar-evar resolution: firstGravatar Hugo Herbelin2014-12-15
* Failing on unbound notation variable in notation level modifiersGravatar Hugo Herbelin2014-12-15
* New try on Fixing an evar_map bug revealed by commit 603b66f81 onGravatar Hugo Herbelin2014-12-15
* Tests for #3848 and #3854.Gravatar Hugo Herbelin2014-12-15
* Documenting check_record + changing a possibly undefined int into int option.Gravatar Hugo Herbelin2014-12-15
* About now accepts hypothesis names and goal selector.Gravatar Pierre Courtieu2014-12-15
* Fix treatment of universe context in typecheck inductive (was addedGravatar Matthieu Sozeau2014-12-15
* Tests for Searchxxx commands added and modified.Gravatar Pierre Courtieu2014-12-15
* Fixing bug #3865.Gravatar Pierre-Marie Pédrot2014-12-15
* Util.un_op -> Option.defaultGravatar Pierre Boutillier2014-12-14
* Fix merging of name maps in union of universe contexts.Gravatar Matthieu Sozeau2014-12-14
* Fixing bug #3858 and #3817 in one stroke.Gravatar Pierre-Marie Pédrot2014-12-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 02:02:33 +0000