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
*
test suite for coq_makefile
Enrico Tassi
2017-05-23
*
Merge PR#661: Added a test for #4765 (an example of printing abbreviation wit...
Maxime Dénès
2017-05-23
|
\
*
\
Merge PR#657: [test-suite] Add tests for goal printing.
Maxime Dénès
2017-05-23
|
\
\
|
|
*
Added a test for #4765 (an example of printing abbreviation with binders).
Hugo Herbelin
2017-05-20
|
|
/
|
/
|
*
|
Merge PR#474: A fix for #5390 (a useful error on used introduction names was ...
Maxime Dénès
2017-05-20
|
\
\
|
|
*
[test-suite] Add tests for goal printing.
Emilio Jesus Gallego Arias
2017-05-20
|
|
/
|
/
|
*
|
Re-adding explicit dependency of misc universe test into all_stdlib.v.
Hugo Herbelin
2017-05-19
|
*
A fix for #5390 (a useful error on used introduction names was masked).
Hugo Herbelin
2017-05-17
*
|
Merge PR#633: An extension of EXTEND and notations to make standard parsing t...
Maxime Dénès
2017-05-17
|
\
\
|
|
/
|
/
|
*
|
Merge PR#457: Adding an even more compact goal hyps mode.
Maxime Dénès
2017-05-17
|
\
\
*
\
\
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-05-17
|
\
\
\
*
\
\
\
Merge PR#620: Reorganization of the layout for miscellaneous tests
Maxime Dénès
2017-05-17
|
\
\
\
\
|
|
|
|
*
Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.
Hugo Herbelin
2017-05-16
|
|
_
|
_
|
/
|
/
|
|
|
|
|
|
*
Simplified compaction criterion + tests.
Pierre Courtieu
2017-05-16
|
|
*
|
Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).
Hugo Herbelin
2017-05-16
|
|
*
|
Fixing a bug with nested "as" clauses in "match".
Hugo Herbelin
2017-05-16
*
|
|
|
Merge PR#594: An example showing the benefit of Econstr
Maxime Dénès
2017-05-11
|
\
\
\
\
*
\
\
\
\
Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 a...
Maxime Dénès
2017-05-11
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR#201: Transparent abstract
Maxime Dénès
2017-05-11
|
\
\
\
\
\
\
|
|
|
|
*
|
|
Moving code for miscellaneous tests to specific files.
Hugo Herbelin
2017-05-10
|
|
|
|
*
|
|
A more regular naming of variables in test-suite Makefile.
Hugo Herbelin
2017-05-10
|
|
|
|
*
|
|
Adding tests for testing exit status and #use"include".
Hugo Herbelin
2017-05-10
|
|
|
|
*
|
|
Cleaning old untested not any more interesting testing files.
Hugo Herbelin
2017-05-10
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR#558: Adding a fold_glob_constr_with_binders combinator
Maxime Dénès
2017-05-05
|
\
\
\
\
\
\
|
|
|
|
*
|
|
Adding a test-suite pattern-unification example that Econstr fixed.
Hugo Herbelin
2017-05-05
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR#544: Anonymous universes
Maxime Dénès
2017-05-05
|
\
\
\
\
\
\
|
|
|
|
|
*
|
FIx bug #5300: uncaught exception in "Print Assumptions".
Cyprien Mangin
2017-05-03
*
|
|
|
|
|
|
Merge PR#541: Fixing "decide equality" bug #5449
Maxime Dénès
2017-05-03
|
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
Type@{_} should not produce a flexible algebraic universe.
Gaetan Gilbert
2017-05-03
|
|
*
|
|
|
|
Allow flexible anonymous universes in instances and sorts.
Gaetan Gilbert
2017-05-03
*
|
|
|
|
|
|
Merge PR#411: Mention template polymorphism in the documentation.
Maxime Dénès
2017-05-03
|
\
\
\
\
\
\
\
|
|
_
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
*
Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions with...
Maxime Dénès
2017-05-02
|
|
|
|
|
|
|
\
|
|
|
|
|
|
*
\
Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite files
Maxime Dénès
2017-05-02
|
|
|
|
|
|
|
\
\
|
|
|
|
|
|
*
|
|
Fixing Set Rewriting Schemes bugs introduced in v8.5.
Hugo Herbelin
2017-05-01
|
|
|
|
|
|
|
*
|
remove unneeded -emacs flag to coq-prog-args
Paul Steckler
2017-05-01
|
|
|
|
|
|
|
|
*
Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
Hugo Herbelin
2017-05-01
|
|
|
|
|
|
|
|
*
Really fixing #2602 which was wrongly working because of #5487 hiding the cause.
Hugo Herbelin
2017-05-01
|
|
|
|
|
|
|
|
/
|
|
|
|
|
|
|
/
|
*
|
|
|
|
|
|
|
Fix bug #5501: Universe polymorphism breaks proof involving auto.
Pierre-Marie Pédrot
2017-04-30
|
|
*
|
|
|
|
|
Fixing "decide equality"'s bug #5449.
Hugo Herbelin
2017-04-30
|
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
*
|
Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."
Maxime Dénès
2017-04-28
|
|
|
|
|
|
/
|
|
|
|
|
*
Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
Hugo Herbelin
2017-04-28
*
|
|
|
|
|
Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...
Maxime Dénès
2017-04-28
|
\
\
\
\
\
\
|
|
|
|
|
|
*
Test for bug #5193: Uncaught exception Class_tactics.Search.ReachedLimitEx.
Pierre-Marie Pédrot
2017-04-27
|
|
|
|
|
*
|
Test surgical use of beta-iota in the type of variables coming from
Hugo Herbelin
2017-04-27
|
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-04-27
|
\
\
\
\
\
\
|
|
|
_
|
_
|
_
|
/
|
|
/
|
|
|
|
|
|
|
|
|
*
Add transparent_abstract tactic
Jason Gross
2017-04-25
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR#574: Fix bug #5476: Ltac has an inconsistent view of hypotheses.
Maxime Dénès
2017-04-24
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR#565: Remove VernacError
Maxime Dénès
2017-04-24
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge branch v8.6 into trunk
Hugo Herbelin
2017-04-22
|
\
\
\
\
\
\
\
|
|
*
|
|
|
|
|
Remove VernacError
Gaetan Gilbert
2017-04-21
|
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
[next]
Enrico Tassi
Maxime Dénès
Hugo Herbelin
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Pierre Courtieu
Cyprien Mangin
Gaetan Gilbert
Paul Steckler
Jason Gross