coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #768: Omega and romega know about context definitions (fix old bug 148)	Maxime Dénès	2017-10-10
\|\
* \	Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type "_som...	Maxime Dénès	2017-10-06
\|\ \
* \ \	Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ...	Maxime Dénès	2017-10-06
\|\ \ \
* \ \ \	Merge PR #1124: Extraction: reduce atomic eta-redexes (solves indirectly BZ#4...	Maxime Dénès	2017-10-06
\|\ \ \ \
\| \| \| \| *	Omega now aware of context variables with bodies (in type Z or nat) (fix bug ...	Pierre Letouzey	2017-10-05
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	Merge PR #1102: On the detection of evars which "advanced" (and a fix to BZ#5...	Maxime Dénès	2017-10-05
\|\ \ \ \
\| \| * \| \|	Extraction: reduce eta-redexes whose cores are atomic (solves indirectly BZ#4...	Pierre Letouzey	2017-10-05
\| \|/ / / \|/\| \| \|
\| \| \| *	Fixing BZ#5769 (variable of type "_something" was named after invalid "_").	Hugo Herbelin	2017-10-05
\| \| * \|	Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).	Hugo Herbelin	2017-10-05
\| \| \|/
* \| \|	Merge PR #1006: fix: ssrmatching and primitive projections	Maxime Dénès	2017-10-04
\|\ \ \
* \ \ \	Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial).	Maxime Dénès	2017-10-04
\|\ \ \ \ \| \|_\|_\|/ \|/\| \| \|
\| \| \| *	Moving setting of "cleared" evar flag directly in Evd.restrict.	Hugo Herbelin	2017-09-27
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ...	Maxime Dénès	2017-09-25
\|\ \ \
* \ \ \	Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4...	Maxime Dénès	2017-09-25
\|\ \ \ \
\| \| * \| \|	Fixing #5755 (discharging of inductive types not correct with let-ins).	Hugo Herbelin	2017-09-23
\| \|/ / / \|/\| \| \|
\| * \| \|	Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).	Hugo Herbelin	2017-09-23
* \| \| \|	A possible fix to BZ#5750 (ability to print context of ltac subterm match).	Hugo Herbelin	2017-09-21
\|/ / /
\| \| *	ssr: fix canonical strucut key comparison with primproj on	Enrico Tassi	2017-09-20
\| * \|	Fixing bug #5741 (anomaly in info_trivial).	Hugo Herbelin	2017-09-19
\|/ /
* \|	Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).	Maxime Dénès	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
\|\ \ \ \
\| \| \| \| *	Avoid extra failure in the "constructor" tactic (bug #5666).	Guillaume Melquiond	2017-09-14
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	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
\|\ \ \ \ \ \
\| \| \| \| \| \| *	Fixing part of #5707 (allowing destruct to use non dependent case analysis).	Hugo Herbelin	2017-08-30
\| \| \| * \| \| \|	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 #773: [flags] Remove XML output flag.	Maxime Dénès	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
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #942: solving b1859	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
\|\ \ \ \
\| \| * \| \|	Adding a test for BZ#1859 as suggested by @tchajed.	Théo Zimmermann	2017-08-15
\| \| \| * \|	[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
\|\ \ \ \ \ \
* \| \| \| \| \| \|	closing bug 5315	Julien Forest	2017-07-29
\| \|_\|_\|_\|/ / \|/\| \| \| \| \|
\| \| \| * \| \|	Fixing bug #5671 (specialize unclean wrt Metas).	Hugo Herbelin	2017-07-27
\| \|_\|/ / / \|/\| \| \| \|
\| \| * \| \|	test-suite: more use of the new command Extraction TestCompile	Pierre Letouzey	2017-07-27
\| \| * \| \|	Enrich test file 4720.v with a compilation test of the extracted code	Pierre Letouzey	2017-07-26
\| \|/ / / \|/\| \| \|
\| * \| \|	adding a test-suite file 4709.v (thanks to the new command Extraction TestCom...	Pierre Letouzey	2017-07-26
\|/ / /