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
*
Remove some dead code and add test-suite file.
Matthieu Sozeau
2015-02-16
*
Add test-suite file for #3960.
Matthieu Sozeau
2015-02-16
*
Test for bug #3922.
Pierre-Marie Pédrot
2015-02-16
*
Fixing bug #4035 (support for dependent destruction within ltac code).
Hugo Herbelin
2015-02-16
*
Test for #2946 (trunk bug with let's in unification).
Hugo Herbelin
2015-02-16
*
Fixing test for bug #3944.
Pierre-Marie Pédrot
2015-02-16
*
Test for bug #3944.
Pierre-Marie Pédrot
2015-02-16
*
Undo: back to 8.4 semantics (Close #3514)
Enrico Tassi
2015-02-15
*
Fix test-suite file. Check that definitions do work when sharing is
Matthieu Sozeau
2015-02-15
*
Test for bug #3490.
Pierre-Marie Pédrot
2015-02-15
*
Test for bug #3916.
Pierre-Marie Pédrot
2015-02-15
*
Fixing test-suite.
Pierre-Marie Pédrot
2015-02-15
*
Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior
Enrico Tassi
2015-02-14
*
Test for bug #4016.
Pierre-Marie Pédrot
2015-02-14
*
Univs: fix bug #3755. We were missing refreshements of universes in
Matthieu Sozeau
2015-02-14
*
Univs: When computing the level of an inductive including indices, lets
Matthieu Sozeau
2015-02-14
*
Fix test-suite file to finish
Matthieu Sozeau
2015-02-13
*
Fixed test-suite file, that should always work.
Matthieu Sozeau
2015-02-12
*
Add test-suite files for closed bugs.
Matthieu Sozeau
2015-02-12
*
COMPATIBILITY: add note about the change of behavior of Instance foo :=
Matthieu Sozeau
2015-02-12
*
Univs: fix bug #4031: wrong folding of sigma in change.
Matthieu Sozeau
2015-02-12
*
Adding test for bug #3786.
Pierre-Marie Pédrot
2015-02-11
*
Adding a test-suite for tactic notation naming.
Pierre-Marie Pédrot
2015-02-11
*
Adding test for bug #3900.
Pierre-Marie Pédrot
2015-02-11
*
Fixing #4001 (missing type constraints when building return clause of match).
Hugo Herbelin
2015-02-10
*
Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ...
Hugo Herbelin
2015-02-10
*
Fixing #4018 (uncaught exception on non-equality in intros [=]).
Hugo Herbelin
2015-02-10
*
Test for bug #4012.
Pierre-Marie Pédrot
2015-02-10
*
Test for bug #3798.
Pierre-Marie Pédrot
2015-01-25
*
There was one more universe needed due to the use of now non-universe-polymor...
Matthieu Sozeau
2015-01-18
*
Back to 4 expected universes.
Matthieu Sozeau
2015-01-17
*
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-17
*
Revert "Adapting two files from test-suite to now forbidden Require's in modu...
Maxime Dénès
2015-01-17
*
Revert "Update test for #3363 now that Require is forbidden inside modules."
Maxime Dénès
2015-01-17
*
Revert "Fix files in test-suite having to do with Require inside modules."
Maxime Dénès
2015-01-17
*
Univs: Fix alias computation for VMs, computation of normal form of
Matthieu Sozeau
2015-01-17
*
Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"
Matthieu Sozeau
2015-01-16
*
TCs: Properly handle Hint Extern with conclusions of the form _ -> _
Matthieu Sozeau
2015-01-13
*
Fix test-suite file, we were testing that no anomaly was raised
Matthieu Sozeau
2015-01-13
*
Fix files in test-suite having to do with Require inside modules.
Maxime Dénès
2015-01-12
*
Update headers.
Maxime Dénès
2015-01-12
*
Update test for #3363 now that Require is forbidden inside modules.
Maxime Dénès
2015-01-12
*
Fixing name of evars in output test Notation.v.
Hugo Herbelin
2015-01-12
*
Extraction: discard code unnecessary to fulfill a module signature
Pierre Letouzey
2015-01-11
*
STM: fix handling of side effects in vio2vo
Enrico Tassi
2015-01-09
*
rename: vi -> vio
Enrico Tassi
2015-01-06
*
Fixing test for bug #2830.
Pierre-Marie Pédrot
2015-01-06
*
kernel/ind Change interface of declare_mind and declare_mutual
Matthieu Sozeau
2015-01-05
*
Adapting two files from test-suite to now forbidden Require's in modules.
Hugo Herbelin
2015-01-04
*
Fixing #3896 (incorrect sigma given to printer).
Hugo Herbelin
2015-01-03
[next]