aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Code cleaning in VM (with Benjamin).Gravatar Maxime Dénès2015-10-09
* Minor typo in universe polymorphism doc.Gravatar Maxime Dénès2015-10-09
* Refine fix for handling of the universe contexts of hints, depending onGravatar Matthieu Sozeau2015-10-09
* Fix CFGV contrib: handling of global hints introducing global universes.Gravatar Matthieu Sozeau2015-10-09
* Fix Next Obligation to not raise an anomaly in case of mutualGravatar Matthieu Sozeau2015-10-09
* Fix inference of return clause raising a type error.Gravatar Matthieu Sozeau2015-10-09
* STM: Work around an occasional crash in dot (debug output)Gravatar Alec Faithfull2015-10-09
* TQueue: Allow some tasks to be saved when clearing a TQueueGravatar Alec Faithfull2015-10-09
* TQueue: Expose the length of TQueuesGravatar Alec Faithfull2015-10-09
* STM: Added functions for saving and restoring the internal stateGravatar Alec Faithfull2015-10-09
* STM: Pass exception information to unreachable_state_hook functionsGravatar Alec Faithfull2015-10-09
* Remove misleading warning (Close #4365)Gravatar Enrico Tassi2015-10-09
* Univs: fix bug #3807Gravatar Matthieu Sozeau2015-10-08
* Allowing empty bound universe variables.Gravatar Pierre-Marie Pédrot2015-10-08
* Univs: fix bug #4161.Gravatar Matthieu Sozeau2015-10-08
* Axioms now support the universe binding syntax.Gravatar Pierre-Marie Pédrot2015-10-08
* f_equal fix continued: do a refresh_universes as before.Gravatar Matthieu Sozeau2015-10-08
* aux_file: export API to ease writing of a Proof Using annotator.Gravatar Enrico Tassi2015-10-08
* Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
* term_typing: strengthen discharging codeGravatar Enrico Tassi2015-10-08
* CThread: blocking read + threads now worksGravatar Enrico Tassi2015-10-08
* Spawn: use each socket exclusively for writing or readingGravatar Enrico Tassi2015-10-08
* STM: for PIDE based UIs, edit_at requires no Reach.known_stateGravatar Enrico Tassi2015-10-08
* Future: make not-here/not-ready messages customizableGravatar Enrico Tassi2015-10-08
* STM: fix backtrace handlingGravatar Enrico Tassi2015-10-08
* Goptions: new value type: optional stringGravatar Enrico Tassi2015-10-08
* Remove the "exists" overrides from Program. (Fix bug #4360)Gravatar Guillaume Melquiond2015-10-07
* Fix bug #4069: f_equal regression.Gravatar Matthieu Sozeau2015-10-07
* Univs: fix FingerTree contrib.Gravatar Matthieu Sozeau2015-10-07
* Test for record syntax parsing.Gravatar Pierre-Marie Pédrot2015-10-07
* Record fields accept an optional final semicolon separator.Gravatar Pierre-Marie Pédrot2015-10-07
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Fixing emacs output in debugging mode.Gravatar Pierre Courtieu2015-10-06
* Univs (pretyping): call vm_compute/native_compute with the currentGravatar Matthieu Sozeau2015-10-06
* Fix bug #4354: interpret hints in the right env and sigma.Gravatar Matthieu Sozeau2015-10-06
* Univs: fix bug #4288, Print Sorted generated backward < constraints.Gravatar Matthieu Sozeau2015-10-05
* Univs: fix printing bug #3797.Gravatar Matthieu Sozeau2015-10-05
* Update the .mailmap file.Gravatar Guillaume Melquiond2015-10-05
* Univs: fix handling of evar_map in identity coercion construction.Gravatar Matthieu Sozeau2015-10-05
* Fix typo. (Fix bug #4355)Gravatar Guillaume Melquiond2015-10-04
* Mark the Coq.Compat files for documentation. (Fix bug #4353)Gravatar Guillaume Melquiond2015-10-02
* Updating versions history with data from Gérard.Gravatar Hugo Herbelin2015-10-02
* Fixing error messages about Hint.Gravatar Hugo Herbelin2015-10-02
* Improving reference manual in that auto uses simple apply rather than apply.Gravatar Hugo Herbelin2015-10-02
* Update the history of versions with recent versions.Gravatar Hugo Herbelin2015-10-02
* Univs: Change intf of push_named_def to return the computed universeGravatar Matthieu Sozeau2015-10-02
* Univs: refined handling of assumptionsGravatar Matthieu Sozeau2015-10-02
* Univs: fix checker generating undeclared universes.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix test-suite file for #4287, now properly rejected.Gravatar Matthieu Sozeau2015-10-02
* Univs: Remove test-suite file #3309Gravatar Matthieu Sozeau2015-10-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 19:06:55 +0000