aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2015-10-02Univs: fix Show Universes.Matthieu Sozeau
2015-10-02Univs: fix handling of side effects/delayed proofsMatthieu Sozeau
2015-10-02Univs: handle side-effects of futures correctly in kernel.Matthieu Sozeau
2015-10-02Univs: fix environment handling in scheme building.Matthieu Sozeau
2015-10-02discriminate: Do fresh_global in the right env in presence of side-effects.Matthieu Sozeau
2015-10-02Univs: fixed bug 2584, correct universe found for mutual inductive.Matthieu Sozeau
2015-10-02Univs: fix Universe vernacular, fix bug #4287.Matthieu Sozeau
2015-10-02Univs: fix after rebase (from_ctx/from_env)Matthieu Sozeau
2015-10-02Univs: fixed bug #4328.Matthieu Sozeau
2015-10-02Univs: fix many evar_map initializations and leaks.Matthieu Sozeau
2015-10-02Univs (pretyping): allow parsing and decl of Top.nMatthieu Sozeau
2015-10-02Univs (evd): deal with global universes and sideffMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 04:22:36 +0000