aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Univs: fix test-suite file (4301 is invalid, but a good regression test)Gravatar Matthieu Sozeau2015-10-02
* Fix after rebase...Gravatar Matthieu Sozeau2015-10-02
* Univs: forgot a substitution in mod_typing.Gravatar Matthieu Sozeau2015-10-02
* Univs: correct handling of with in modulesGravatar Matthieu Sozeau2015-10-02
* Univs: the stdlib now needs 5 universesGravatar Matthieu Sozeau2015-10-02
* Univs: fix bug #4251, handling of template polymorphic constants.Gravatar Matthieu Sozeau2015-10-02
* Univs: update checkerGravatar Matthieu Sozeau2015-10-02
* Univs: fixed 3685 by side-effect :)Gravatar Matthieu Sozeau2015-10-02
* Univs: minor fixes to test-suite filesGravatar Matthieu Sozeau2015-10-02
* Univs: fix handling of evd's universes and side effects in build_by_tacticGravatar Matthieu Sozeau2015-10-02
* Univs: fix semantics of Type in proof mode in universe-polymorphic modeGravatar Matthieu Sozeau2015-10-02
* Univs: fix minimization to allow lowering a universe to Set, not Prop.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix inference of the lowest sort for records.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix subtyping of polymorphic parameters.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix evar_map handling in Hint processing.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix test-suite file for HoTT/coq bug #120Gravatar Matthieu Sozeau2015-10-02
* Univs: test-suite file for bug #2016Gravatar Matthieu Sozeau2015-10-02
* Univs: test-suite file for #4301, subtyping of poly parametersGravatar Matthieu Sozeau2015-10-02
* Univs: uncovered bug in strengthening of opaque polymorphic definitions.Gravatar Matthieu Sozeau2015-10-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 08:21:19 +0000