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
*
Using x in output test-suite Cases.v (cosmetic).
Hugo Herbelin
2015-12-05
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-03
|
\
|
*
Adding a target report to test-suite's Makefile to get a short summary.
Hugo Herbelin
2015-12-02
|
*
Improving syntax of pat/constr introduction pattern so that
Hugo Herbelin
2015-12-02
|
*
Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.
Hugo Herbelin
2015-12-02
*
|
New algorithm for universe cycle detections.
Jacques-Henri Jourdan
2015-12-01
|
*
Test for bug #4149.
Pierre-Marie Pédrot
2015-11-30
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-29
|
\
|
|
*
Test-suite files for closed bugs
Matthieu Sozeau
2015-11-28
|
*
Closed bugs.
Matthieu Sozeau
2015-11-28
|
*
Univs: entirely disallow instantiation of polymorphic constants with
Matthieu Sozeau
2015-11-27
|
*
Fixing the "parsing rules with idents later declared as keywords" problem.
Hugo Herbelin
2015-11-26
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-26
|
\
|
|
*
Fixing a vm_compute bug in the presence of let-ins among the
Hugo Herbelin
2015-11-22
|
*
Fixing a bug of adjust_subst_to_rel_context.
Hugo Herbelin
2015-11-22
|
*
Fixing kernel bug in typing match with let-ins in the arity.
Hugo Herbelin
2015-11-22
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-20
|
\
|
|
*
Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.
Pierre-Marie Pédrot
2015-11-19
|
*
Fixing logical bugs in the presence of let-ins in computiong primitive
Hugo Herbelin
2015-11-18
*
|
Fixing output test Cases.v.
Pierre-Marie Pédrot
2015-11-15
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-15
|
\
|
|
*
Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.
Pierre-Marie Pédrot
2015-11-12
|
*
Fixed test-suite file for bug #3998.
Matthieu Sozeau
2015-11-12
|
*
Now closed.
Matthieu Sozeau
2015-11-11
|
*
Fix bug #3257, setoid_reflexivity should fail if not completing the goal.
Matthieu Sozeau
2015-11-11
|
*
Fix bug #4293: ensure let-ins do not contain algebraic universes in
Matthieu Sozeau
2015-11-11
|
*
Fixing bug #3554: Anomaly: Anonymous implicit argument.
Pierre-Marie Pédrot
2015-11-11
*
|
Updating test-suite after Bracketing Last Introduction Pattern set by
Hugo Herbelin
2015-11-10
*
|
Revert "Fixing #1225: we now skip the canonically built binding contexts of"
Hugo Herbelin
2015-11-10
*
|
Fixing #1225: we now skip the canonically built binding contexts of
Hugo Herbelin
2015-11-10
*
|
Merge origin/v8.5 into trunk
Hugo Herbelin
2015-11-10
|
\
|
|
*
Test for bug #4404.
Pierre-Marie Pédrot
2015-11-10
*
|
Adapting output test inference.v after c23f0cab6 (experimenting
Hugo Herbelin
2015-11-08
|
*
Fixing output test Existentials.v after eec77191b.
Hugo Herbelin
2015-11-07
|
*
Tests for syntax "Show id" and [id]:tac (shelved or not).
Hugo Herbelin
2015-11-07
*
|
Merge remote-tracking branch 'origin/v8.5' into upstream-trunk
Hugo Herbelin
2015-11-07
|
\
|
|
*
Fixing complexity file f_equal.v.
Hugo Herbelin
2015-11-06
|
*
Fixing complexity issue with f_equal. Thanks to J.-H. Jourdan
Hugo Herbelin
2015-11-06
|
*
Add test-suite file for #4273.
Matthieu Sozeau
2015-11-05
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
|
\
|
|
*
Univs: missing checks in evarsolve with candidates and missing a
Matthieu Sozeau
2015-11-04
|
*
Hint Cut documentation and cleanup of printing (was duplicated and
Matthieu Sozeau
2015-11-04
|
*
Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusion
Matthieu Sozeau
2015-11-04
|
*
Test file for #4397.
Maxime Dénès
2015-11-04
|
*
Fix bug #4151: discrepancy between exact and eexact/eassumption.
Matthieu Sozeau
2015-11-02
|
*
Refresh rigid universes as well, and in 8.4 compatibility mode,
Matthieu Sozeau
2015-11-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-30
|
\
|
|
*
Handle side-effects of Vernacular commands inside proofs better, so that
Matthieu Sozeau
2015-10-29
|
*
Fixing another instance of bug #3267 in eauto, this time in the
Hugo Herbelin
2015-10-29
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
[next]