aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\
* \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-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
| | * Fix test-suite file for bug #3777Gravatar Matthieu Sozeau2015-10-02
| | * Fix test-suite file: failing earlier as expected.Gravatar Matthieu Sozeau2015-10-02
| | * Fix test-suite fileGravatar Matthieu Sozeau2015-10-02
| | * Univs: correcly compute the levels of records when they fall in Prop.Gravatar Matthieu Sozeau2015-10-02
| | * Univs/program: handle side effects in obligations.Gravatar Matthieu Sozeau2015-10-02
| | * Univs: fix Show Universes.Gravatar Matthieu Sozeau2015-10-02
| | * Univs: fix handling of side effects/delayed proofsGravatar Matthieu Sozeau2015-10-02
| | * Univs: handle side-effects of futures correctly in kernel.Gravatar Matthieu Sozeau2015-10-02
| | * Univs: fix environment handling in scheme building.Gravatar Matthieu Sozeau2015-10-02
| | * discriminate: Do fresh_global in the right env in presence of side-effects.Gravatar Matthieu Sozeau2015-10-02
| | * Univs: fixed bug 2584, correct universe found for mutual inductive.Gravatar Matthieu Sozeau2015-10-02
| | * Univs: fix Universe vernacular, fix bug #4287.Gravatar Matthieu Sozeau2015-10-02
| | * Univs: fix after rebase (from_ctx/from_env)Gravatar Matthieu Sozeau2015-10-02
| | * Univs: fixed bug #4328.Gravatar Matthieu Sozeau2015-10-02
| | * Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
| | * Univs (pretyping): allow parsing and decl of Top.nGravatar Matthieu Sozeau2015-10-02
| | * Univs (evd): deal with global universes and sideffGravatar Matthieu Sozeau2015-10-02
| | * Univs: fix evar_map initialization in newring.Gravatar Matthieu Sozeau2015-10-02
| | * Univs: fix evar_map leaks bugs in FunctionGravatar Matthieu Sozeau2015-10-02
| | * Univs: fix an evar leak in congruenceGravatar Matthieu Sozeau2015-10-02
| | * Univs: minimization, adapt to graph invariants.Gravatar Matthieu Sozeau2015-10-02
| | * Univs (kernel) adapt to new invariantsGravatar Matthieu Sozeau2015-10-02
| | * Univs: module constraints move to universe contexts as they mightGravatar Matthieu Sozeau2015-10-02
| | * Remove Print Universe directive.Gravatar Matthieu Sozeau2015-10-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 03:55:04 +0000