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
\|\
* \|	[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.	Emilio Jesus Gallego Arias	2017-10-05
\| *	romega: takes advantage of context variables with body	Pierre Letouzey	2017-10-05
\|/
*	Merge PR #1101: Fixing an old proof engine bug in collecting evars with clear...	Maxime Dénès	2017-10-05
\|\
* \|	[vernac] Remove `Qed exporting` syntax.	Emilio Jesus Gallego Arias	2017-09-29
\| *	Fixing an old bug in collecting evars with cleared context.	Hugo Herbelin	2017-09-27
\|/
*	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès	2017-09-26
\|\
* \|	Fixing _rect bug for inductive types with let-ins and non-rec uniform params.	Hugo Herbelin	2017-09-23
\| *	test-suite: polymorphism	Matthieu Sozeau	2017-09-19
\| *	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 #920: kernel: bugfix in filter_stack_domain.	Maxime Dénès	2017-09-19
\|\ \ \| \|/ \|/\|
\| *	Add test-suite script by Cyprien Mangin	Matthieu Sozeau	2017-09-18
* \|	Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...	Maxime Dénès	2017-09-15
\|\ \
* \| \|	Fixing little inaccuracy in coercions to ident or name.	Hugo Herbelin	2017-09-12
* \| \|	Merge PR #830: Moving assert (the "Cut" rule) to new proof engine	Maxime Dénès	2017-08-29
\|\ \ \
\| \| * \|	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin	2017-08-21
\| \|/ / \|/\| \|
* \| \|	Merge PR #864: Some cleanups after cumulativity for inductive types	Maxime Dénès	2017-08-16
\|\ \ \
\| * \| \|	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
\| \| \|/ \| \|/\|
* \| \|	test-suite: more use of the new command Extraction TestCompile	Pierre Letouzey	2017-07-27
* \| \|	test-suite/success/extraction.v : add some Extraction TestCompile	Pierre Letouzey	2017-07-26
\|/ /
* \|	Remove non-terminating Timeout tests from Hints.v.	Maxime Dénès	2017-07-20
* \|	Getting rid of abstraction breaking code in tclABSTRACT.	Pierre-Marie Pédrot	2017-07-14
* \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| *	Reorganizing functions to find the relative position of an hypothesis.	Hugo Herbelin	2017-06-25
\| *	Moving "assert" (internally "Cut") to the new proof engine.	Hugo Herbelin	2017-06-25
* \|	Add test-suite file for funind, extraction with compat 8.6	Jason Gross	2017-06-22
\|/
*	Merge PR#807: romega: fix a slowdown	Maxime Dénès	2017-06-20
\|\
\| *	romega: avoid potential slowdown when changing concl by reified version	Pierre Letouzey	2017-06-16
* \|	Fix a bug in cumulativity	Amin Timany	2017-06-16
* \|	Move (part of) tests from checker to success	Amin Timany	2017-06-16
* \|	Disable debug printing	Amin Timany	2017-06-16
* \|	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
* \|	Fix bugs	Amin Timany	2017-06-16
\|/
*	Merge PR#375: Deprecation	Maxime Dénès	2017-06-15
\|\
* \	Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").	Maxime Dénès	2017-06-14
\|\ \
* \| \|	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	2017-06-14
\| \| *	Remove support for Coq 8.4.	Guillaume Melquiond	2017-06-14
\| \|/ \|/\|
* \|	Merge PR#498: Bignums as a separate opam package	Maxime Dénès	2017-06-14
\|\ \
* \ \	Merge PR#385: Equality of sigma types	Maxime Dénès	2017-06-13
\|\ \ \
\| \| * \|	BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)	Pierre Letouzey	2017-06-13
\| \|/ / \|/\| \|
\| \| *	A fix to #5414 (ident bound by ltac names now known for "match").	Hugo Herbelin	2017-06-09
\| \|/ \|/\|
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-06-08
\|\ \
* \ \	Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...	Maxime Dénès	2017-06-06
\|\ \ \
* \ \ \	Merge PR#600: Some factorizations of ltac interpretation functions between ss...	Maxime Dénès	2017-06-06
\|\ \ \ \
* \| \| \| \|	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
* \| \| \| \|	Merge PR#449: make specialize smarter (bug 5370).	Maxime Dénès	2017-06-01
\|\ \ \ \ \