index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
Univs: fix test-suite file (4301 is invalid, but a good regression test)
Matthieu Sozeau
2015-10-02
*
Fix after rebase...
Matthieu Sozeau
2015-10-02
*
Univs: forgot a substitution in mod_typing.
Matthieu Sozeau
2015-10-02
*
Univs: correct handling of with in modules
Matthieu Sozeau
2015-10-02
*
Univs: the stdlib now needs 5 universes
Matthieu Sozeau
2015-10-02
*
Univs: fix bug #4251, handling of template polymorphic constants.
Matthieu Sozeau
2015-10-02
*
Univs: update checker
Matthieu Sozeau
2015-10-02
*
Univs: fixed 3685 by side-effect :)
Matthieu Sozeau
2015-10-02
*
Univs: minor fixes to test-suite files
Matthieu Sozeau
2015-10-02
*
Univs: fix handling of evd's universes and side effects in build_by_tactic
Matthieu Sozeau
2015-10-02
*
Univs: fix semantics of Type in proof mode in universe-polymorphic mode
Matthieu Sozeau
2015-10-02
*
Univs: fix minimization to allow lowering a universe to Set, not Prop.
Matthieu Sozeau
2015-10-02
*
Univs: fix inference of the lowest sort for records.
Matthieu Sozeau
2015-10-02
*
Univs: fix subtyping of polymorphic parameters.
Matthieu Sozeau
2015-10-02
*
Univs: fix evar_map handling in Hint processing.
Matthieu Sozeau
2015-10-02
*
Univs: fix test-suite file for HoTT/coq bug #120
Matthieu Sozeau
2015-10-02
*
Univs: test-suite file for bug #2016
Matthieu Sozeau
2015-10-02
*
Univs: test-suite file for #4301, subtyping of poly parameters
Matthieu Sozeau
2015-10-02
*
Univs: uncovered bug in strengthening of opaque polymorphic definitions.
Matthieu Sozeau
2015-10-02
*
Fix test-suite file for bug #3777
Matthieu Sozeau
2015-10-02
*
Fix test-suite file: failing earlier as expected.
Matthieu Sozeau
2015-10-02
*
Fix test-suite file
Matthieu Sozeau
2015-10-02
*
Univs: correcly compute the levels of records when they fall in Prop.
Matthieu Sozeau
2015-10-02
*
Univs/program: handle side effects in obligations.
Matthieu Sozeau
2015-10-02
*
Univs: fix Show Universes.
Matthieu Sozeau
2015-10-02
*
Univs: fix handling of side effects/delayed proofs
Matthieu Sozeau
2015-10-02
*
Univs: handle side-effects of futures correctly in kernel.
Matthieu Sozeau
2015-10-02
*
Univs: fix environment handling in scheme building.
Matthieu Sozeau
2015-10-02
*
discriminate: Do fresh_global in the right env in presence of side-effects.
Matthieu Sozeau
2015-10-02
*
Univs: fixed bug 2584, correct universe found for mutual inductive.
Matthieu Sozeau
2015-10-02
*
Univs: fix Universe vernacular, fix bug #4287.
Matthieu Sozeau
2015-10-02
*
Univs: fix after rebase (from_ctx/from_env)
Matthieu Sozeau
2015-10-02
*
Univs: fixed bug #4328.
Matthieu Sozeau
2015-10-02
*
Univs: fix many evar_map initializations and leaks.
Matthieu Sozeau
2015-10-02
*
Univs (pretyping): allow parsing and decl of Top.n
Matthieu Sozeau
2015-10-02
*
Univs (evd): deal with global universes and sideff
Matthieu Sozeau
2015-10-02
*
Univs: fix evar_map initialization in newring.
Matthieu Sozeau
2015-10-02
*
Univs: fix evar_map leaks bugs in Function
Matthieu Sozeau
2015-10-02
*
Univs: fix an evar leak in congruence
Matthieu Sozeau
2015-10-02
*
Univs: minimization, adapt to graph invariants.
Matthieu Sozeau
2015-10-02
*
Univs (kernel) adapt to new invariants
Matthieu Sozeau
2015-10-02
*
Univs: module constraints move to universe contexts as they might
Matthieu Sozeau
2015-10-02
*
Remove Print Universe directive.
Matthieu Sozeau
2015-10-02
*
Univs: More info for developers.
Matthieu Sozeau
2015-10-02
*
Forcing i > Set for global universes (incomplete)
Matthieu Sozeau
2015-10-02
*
Univs: force all universes to be >= Set.
Matthieu Sozeau
2015-10-02
*
Univs: Fix part of bug #4161
Matthieu Sozeau
2015-10-02
*
Universes: enforce Set <= i for all Type occurrences.
Matthieu Sozeau
2015-10-02
*
Changed status of Info messages from notice to info.
Pierre Courtieu
2015-10-02
*
emacs output mode: Added <infomsg> tag to debug messages.
Pierre Courtieu
2015-10-02
[prev]
[next]