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
*
Allow declaring universe binders with no constraints with @{|}
Gaëtan Gilbert
2017-09-19
*
Allow declaring universe constraints at definition level.
Matthieu Sozeau
2017-09-19
*
Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In...
Maxime Dénès
2017-09-15
|
\
*
\
Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...
Maxime Dénès
2017-09-15
|
\
\
*
\
\
Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match anon...
Maxime Dénès
2017-09-15
|
\
\
\
*
|
|
|
Fixing bug #5693 (treating empty notation format as any format).
Hugo Herbelin
2017-09-12
*
|
|
|
Fixing a bug of recursive notations introduced in dfdaf4de.
Hugo Herbelin
2017-09-12
*
|
|
|
Fixing little inaccuracy in coercions to ident or name.
Hugo Herbelin
2017-09-12
*
|
|
|
Merge PR #1017: Addressing BZ#5713 (classical_left/classical_right artificial...
Maxime Dénès
2017-09-11
|
\
\
\
\
*
\
\
\
\
Merge PR #997: coqdoc: Support comments in verbatim output
Maxime Dénès
2017-09-07
|
\
\
\
\
\
*
|
|
|
|
|
fix test-suite/coq-makefile/findlib-package on windows
Enrico Tassi
2017-09-04
|
|
*
|
|
|
Addressing BZ#5713 (classical_left/classical_right artificially restricted).
Hugo Herbelin
2017-09-03
|
|
/
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #996: Fix BZ#5697: Congruence does not work with primitive projections
Maxime Dénès
2017-08-31
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #995: Program: fix BZ#5683, missing lift when building case predicate
Maxime Dénès
2017-08-31
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flag
Maxime Dénès
2017-08-31
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #958: coq_makefile: build/use .cma for packed plugins too
Maxime Dénès
2017-08-31
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #998: Avoid running interactive tests on Windows.
Maxime Dénès
2017-08-30
|
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
|
|
*
Fixing part of #5707 (allowing destruct to use non dependent case analysis).
Hugo Herbelin
2017-08-30
|
|
*
|
|
|
|
|
|
|
coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxs
Enrico Tassi
2017-08-29
|
*
|
|
|
|
|
|
|
|
Avoid running interactive tests on Windows.
Maxime Dénès
2017-08-29
|
|
|
|
|
*
|
|
|
|
Properly handling parameters of primitive projections in cctac.
Pierre-Marie Pédrot
2017-08-29
|
|
|
|
|
*
|
|
|
|
Fix BZ#5697: Congruence does not work with primitive projections.
Pierre-Marie Pédrot
2017-08-29
|
|
_
|
_
|
_
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur...
Maxime Dénès
2017-08-29
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #830: Moving assert (the "Cut" rule) to new proof engine
Maxime Dénès
2017-08-29
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR #773: [flags] Remove XML output flag.
Maxime Dénès
2017-08-29
|
\
\
\
\
\
\
\
\
\
\
\
|
|
_
|
_
|
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
coq_makefile: use dedicated variable for extra packages
Enrico Tassi
2017-08-29
|
|
|
|
*
|
|
|
|
|
|
coq_makefile: test using findlib's package
Enrico Tassi
2017-08-29
|
|
_
|
_
|
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
coqdoc: Support comments in verbatim output
Tej Chajed
2017-08-29
|
|
|
|
|
|
|
|
_
|
/
|
|
|
|
|
|
|
/
|
|
|
|
|
*
|
|
|
|
|
Adding a test for #5569 (warning about skipping spaces).
Hugo Herbelin
2017-08-29
|
|
|
*
|
|
|
|
|
Dropping former fix to bug #5469 (notation format not recognizing curly braces).
Hugo Herbelin
2017-08-29
|
|
|
*
|
|
|
|
|
A little reorganization of notations + a fix to #5608.
Hugo Herbelin
2017-08-29
|
|
|
|
|
_
|
/
/
/
|
|
|
|
/
|
|
|
|
|
|
|
|
*
|
|
|
primproj: fix bug 5245, hnf on proj with simpl never flag.
Matthieu Sozeau
2017-08-25
|
|
|
|
/
/
/
/
|
|
|
|
*
/
/
Program: fix BZ#5683, missing lift when building case predicate
Matthieu Sozeau
2017-08-24
|
|
|
|
/
/
/
|
|
|
|
|
*
Ensuring all .v files end with a newline to make "sed -i" work better on them.
Hugo Herbelin
2017-08-21
|
|
|
|
|
/
|
|
|
|
/
|
*
|
|
/
|
Fix coqdoc test-suite target on Windows.
Théo Zimmermann
2017-08-21
|
|
_
|
/
/
|
/
|
|
|
*
|
|
|
Merge PR #942: solving b1859
Maxime Dénès
2017-08-16
|
\
\
\
\
*
\
\
\
\
Merge PR #954: Print names of all open blocks
Maxime Dénès
2017-08-16
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #841: Timorous fix of bug #5598 on global existing class in sections
Maxime Dénès
2017-08-16
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords wr...
Maxime Dénès
2017-08-16
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #864: Some cleanups after cumulativity for inductive types
Maxime Dénès
2017-08-16
|
\
\
\
\
\
\
\
\
|
|
|
|
|
*
|
|
|
Adding a test for BZ#1859 as suggested by @tchajed.
Théo Zimmermann
2017-08-15
|
|
|
|
*
|
|
|
|
Print names of all open blocks
Tej Chajed
2017-08-06
|
|
_
|
_
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
[flags] Remove XML output flag.
Emilio Jesus Gallego Arias
2017-08-01
|
|
_
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
*
|
|
|
|
|
|
Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).
Maxime Dénès
2017-08-01
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #926: test-suite uses Extraction TestCompile
Maxime Dénès
2017-08-01
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)
Maxime Dénès
2017-08-01
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #834: Adding support for recursive notations of the form "x , .. , y...
Maxime Dénès
2017-08-01
|
\
\
\
\
\
\
\
\
\
\
|
|
|
|
|
*
|
|
|
|
|
Change the option for cumulativity
Amin Timany
2017-07-31
|
|
|
|
|
*
|
|
|
|
|
Add Jason's example of fun-ext with cumulativity
Amin Timany
2017-07-31
|
|
|
|
|
*
|
|
|
|
|
Add test for NonCumulative inductives
Amin Timany
2017-07-31
[next]
Gaëtan Gilbert
Matthieu Sozeau
Maxime Dénès
Hugo Herbelin
Enrico Tassi
Pierre-Marie Pédrot
Tej Chajed
Matthieu Sozeau
Théo Zimmermann
Emilio Jesus Gallego Arias
Amin Timany