coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| \| * \|	Avoid extra failure in the "constructor" tactic (bug #5666).	Guillaume Melquiond	2017-09-14
\| \|_\|_\|_\|/ / \|/\| \| \| \| \|
\| \| \| \| \| *	Adding a test for utf8 characters in directory names.	Hugo Herbelin	2017-09-13
* \| \| \| \| \|	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
\| \| \| \| \| * \| \| \| \| \| \|	Issue error on monomorphic cumulative inductives	Amin Timany	2017-07-31
\| \| \| \| \| \| \|_\|/ / / / \| \| \| \| \| \|/\| \| \| \| \|
* \| \| \| \| / \| \| \| \| \|	closing bug 5315	Julien Forest	2017-07-29
\| \|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \|	Fixing bug #5671 (specialize unclean wrt Metas).	Hugo Herbelin	2017-07-27
\| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|