index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
Commit message (
Expand
)
Author
Age
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-26
|
\
|
*
Backtracking on interpreting toplevel calls to exact in scope determined
Hugo Herbelin
2015-10-24
|
*
Fixing a bug in reporting ill-formed inductive.
Hugo Herbelin
2015-10-22
|
*
Bug #3956 is fixed.
Matthieu Sozeau
2015-10-21
*
|
Removing test for bug #3956.
Pierre-Marie Pédrot
2015-10-21
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-19
|
\
|
|
*
Test for #4372 (anomaly in inversion in the presence of fake dependency).
Hugo Herbelin
2015-10-19
|
*
Fixing #4198 (continued): not matching within the inner lambdas/let-ins
Hugo Herbelin
2015-10-18
|
*
Test for bug #4325.
Pierre-Marie Pédrot
2015-10-17
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-10-16
|
\
|
|
*
Test file for #4346: Set is no longer of type Type
Maxime Dénès
2015-10-15
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
|
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-12
|
\
|
|
*
Adding test for bug #4366.
Pierre-Marie Pédrot
2015-10-11
|
*
Fixing test-suite
Hugo Herbelin
2015-10-11
|
*
Fixing untimely unexpected warning "Collision between bound variables" (#4317).
Hugo Herbelin
2015-10-11
|
*
Refining 0c320e79ba30 in fixing interpretation of constr under binders
Hugo Herbelin
2015-10-11
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-10
|
\
|
|
*
Refine fix for handling of the universe contexts of hints, depending on
Matthieu Sozeau
2015-10-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
*
Univs: fix bug #4161.
Matthieu Sozeau
2015-10-08
|
*
Proof using: let-in policy, optional auto-clear, forward closure*
Enrico Tassi
2015-10-08
|
*
Fix bug #4069: f_equal regression.
Matthieu Sozeau
2015-10-07
|
*
Test for record syntax parsing.
Pierre-Marie Pédrot
2015-10-07
|
*
Univs: add Strict Universe Declaration option (on by default)
Matthieu Sozeau
2015-10-07
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-06
|
\
|
|
*
Fix bug #4354: interpret hints in the right env and sigma.
Matthieu Sozeau
2015-10-06
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
|
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
\
|
|
*
Univs: fix test-suite file for #4287, now properly rejected.
Matthieu Sozeau
2015-10-02
|
|
*
Univs: Remove test-suite file #3309
Matthieu Sozeau
2015-10-02
|
|
*
Univs: fix test-suite file (4301 is invalid, but a good regression test)
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: fixed 3685 by side-effect :)
Matthieu Sozeau
2015-10-02
|
|
*
Univs: minor fixes to test-suite files
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
|
|
*
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: 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: fixed bug #4328.
Matthieu Sozeau
2015-10-02
|
|
*
Forcing i > Set for global universes (incomplete)
Matthieu Sozeau
2015-10-02
|
|
/
|
*
Test for bug #4347.
Pierre-Marie Pédrot
2015-09-26
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-09-25
|
\
|
[next]