aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Call Evd.nf_constraints only on Univ Poly constantsGravatar Enrico Tassi2014-12-26
* STM: remove dead codeGravatar Enrico Tassi2014-12-26
* Term: include a function to print termsGravatar Enrico Tassi2014-12-26
* Document 6d5b56d971 (forbid Require inside modules).Gravatar Maxime Dénès2014-12-25
* Forbid Require inside interactive modules and module types.Gravatar Maxime Dénès2014-12-25
* Inlining Spawn.kill_if in the one place were it was actually used, thusGravatar Pierre-Marie Pédrot2014-12-25
* STM: cleanup code for AdmittedGravatar Enrico Tassi2014-12-23
* Vi2vo: fix handling of univ constraints coming from the bodyGravatar Enrico Tassi2014-12-23
* Minor modification of CHANGE.Gravatar Pierre Courtieu2014-12-23
* A global [gfail] tactic which works like [fail] except that it fails even if ...Gravatar Arnaud Spiwack2014-12-23
* Remove compatibility layer from Ltac's [fail].Gravatar Arnaud Spiwack2014-12-23
* Fix compilation error in some configurations.Gravatar Arnaud Spiwack2014-12-23
* Dead code in Univ.Gravatar Pierre-Marie Pédrot2014-12-21
* Win32: fix installerGravatar Enrico Tassi2014-12-19
* Install .v and .glob files tooGravatar Enrico Tassi2014-12-19
* Add a backtracking version of Ltac's [match].Gravatar Arnaud Spiwack2014-12-19
* When pretyping [uconstr] closures, don't use the local Ltac variable environm...Gravatar Arnaud Spiwack2014-12-19
* Fixing performance issue of checker validation.Gravatar Pierre-Marie Pédrot2014-12-19
* Fixing checker representation of values.Gravatar Pierre-Marie Pédrot2014-12-19
* update md5 sums to make "make check" workGravatar Enrico Tassi2014-12-19
* Fix sigsegv in checkerGravatar Enrico Tassi2014-12-19
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
* Back to the preferred ?n1:=?n2 order of evar-evar unification which got accid...Gravatar Hugo Herbelin2014-12-19
* Fixing wrong notation level in #3295.Gravatar Hugo Herbelin2014-12-19
* Adds two lemmas about hderror to the List standard library.Gravatar Sébastien Hinderer2014-12-18
* Implement the nodup function on lists and prove associated results.Gravatar Sébastien Hinderer2014-12-18
* Lists: enhanced version of Seb's last commit on Exists/ForallGravatar Pierre Letouzey2014-12-18
* Lists: a few results on Exists and Forall and a bit of code cleanup.Gravatar Sébastien Hinderer2014-12-18
* Fixing checker representation of universe lists.Gravatar Pierre-Marie Pédrot2014-12-18
* Backporting the change in lists of universes to the checker.Gravatar Pierre-Marie Pédrot2014-12-18
* Cleaning up universe list implementation in Univ.Gravatar Pierre-Marie Pédrot2014-12-18
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
* Bug fix (coq_makefile): Adding unix.cma and threads.cma dependencies for gram...Gravatar mlasson2014-12-18
* Fixed bad newlines in output for std output and emacs.Gravatar Pierre Courtieu2014-12-18
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 05:29:14 +0000