aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-10-08STM: fix backtrace handlingEnrico Tassi
2015-10-08Goptions: new value type: optional stringEnrico Tassi
2015-10-07Remove the "exists" overrides from Program. (Fix bug #4360)Guillaume Melquiond
2015-10-07Fix bug #4069: f_equal regression.Matthieu Sozeau
2015-10-07Univs: fix FingerTree contrib.Matthieu Sozeau
2015-10-07Test for record syntax parsing.Pierre-Marie Pédrot
2015-10-07Record fields accept an optional final semicolon separator.Pierre-Marie Pédrot
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-10-06Fixing emacs output in debugging mode.Pierre Courtieu
2015-10-06Univs (pretyping): call vm_compute/native_compute with the currentMatthieu Sozeau
2015-10-06Fix bug #4354: interpret hints in the right env and sigma.Matthieu Sozeau
2015-10-05Univs: fix bug #4288, Print Sorted generated backward < constraints.Matthieu Sozeau
2015-10-05Univs: fix printing bug #3797.Matthieu Sozeau
2015-10-05Update the .mailmap file.Guillaume Melquiond
2015-10-05Univs: fix handling of evar_map in identity coercion construction.Matthieu Sozeau
2015-10-04Fix typo. (Fix bug #4355)Guillaume Melquiond
2015-10-02Mark the Coq.Compat files for documentation. (Fix bug #4353)Guillaume Melquiond
2015-10-02Updating versions history with data from Gérard.Hugo Herbelin
2015-10-02Fixing error messages about Hint.Hugo Herbelin
2015-10-02Improving reference manual in that auto uses simple apply rather than apply.Hugo Herbelin
2015-10-02Update the history of versions with recent versions.Hugo Herbelin
2015-10-02Univs: Change intf of push_named_def to return the computed universeMatthieu Sozeau
2015-10-02Univs: refined handling of assumptionsMatthieu Sozeau
2015-10-02Univs: fix checker generating undeclared universes.Matthieu Sozeau
2015-10-02Univs: fix test-suite file for #4287, now properly rejected.Matthieu Sozeau
2015-10-02Univs: Remove test-suite file #3309Matthieu Sozeau
2015-10-02Univs: fix test-suite file (4301 is invalid, but a good regression test)Matthieu Sozeau
2015-10-02Fix after rebase...Matthieu Sozeau
2015-10-02Univs: forgot a substitution in mod_typing.Matthieu Sozeau
2015-10-02Univs: correct handling of with in modulesMatthieu Sozeau
2015-10-02Univs: the stdlib now needs 5 universesMatthieu Sozeau
2015-10-02Univs: fix bug #4251, handling of template polymorphic constants.Matthieu Sozeau
2015-10-02Univs: update checkerMatthieu Sozeau
2015-10-02Univs: fixed 3685 by side-effect :)Matthieu Sozeau
2015-10-02Univs: minor fixes to test-suite filesMatthieu Sozeau
2015-10-02Univs: fix handling of evd's universes and side effects in build_by_tacticMatthieu Sozeau
2015-10-02Univs: fix semantics of Type in proof mode in universe-polymorphic modeMatthieu Sozeau
2015-10-02Univs: fix minimization to allow lowering a universe to Set, not Prop.Matthieu Sozeau
2015-10-02Univs: fix inference of the lowest sort for records.Matthieu Sozeau
2015-10-02Univs: fix subtyping of polymorphic parameters.Matthieu Sozeau
2015-10-02Univs: fix evar_map handling in Hint processing.Matthieu Sozeau
2015-10-02Univs: fix test-suite file for HoTT/coq bug #120Matthieu Sozeau
2015-10-02Univs: test-suite file for bug #2016Matthieu Sozeau
2015-10-02Univs: test-suite file for #4301, subtyping of poly parametersMatthieu Sozeau
2015-10-02Univs: uncovered bug in strengthening of opaque polymorphic definitions.Matthieu Sozeau
2015-10-02Fix test-suite file for bug #3777Matthieu Sozeau
2015-10-02Fix test-suite file: failing earlier as expected.Matthieu Sozeau
2015-10-02Fix test-suite fileMatthieu Sozeau
2015-10-02Univs: correcly compute the levels of records when they fall in Prop.Matthieu Sozeau
2015-10-02Univs/program: handle side effects in obligations.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 08:39:35 +0000