coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \|	Merge PR #6551: Bracket with goal selector	Maxime Dénès	2018-01-16
\|\ \ \ \| \|/ / \|/\| \|
\| * \|	More tests on brackets with goal selectors (including failures).	Théo Zimmermann	2018-01-15
\| * \|	Add test-suite file for bracket with goal selector.	Théo Zimmermann	2018-01-15
* \| \|	Force polymorphic definitions to have no internal constraints.	Pierre-Marie Pédrot	2018-01-11
\|/ /
\| *	Fix core hint database issue #6521	Anton Trunov	2018-01-03
\|/
*	Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra...	Maxime Dénès	2017-12-18
\|\
* \|	Fix anomaly in [Type foo] command, + print uctx like Check.	Gaëtan Gilbert	2017-12-11
\| *	use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language	Paul Steckler	2017-12-05
\|/
*	Tests for global universe declarations	Matthieu Sozeau	2017-12-01
*	Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as in...	Maxime Dénès	2017-11-30
\|\
* \	Merge PR #6253: Fixing inconsistent associativity of level 10 in the table of...	Maxime Dénès	2017-11-29
\|\ \
\| \| *	Fix (partial) #4878: option to stop autodeclaring axiom as instance.	Gaëtan Gilbert	2017-11-28
\| \|/ \|/\|
\| *	Fixing associativity registered for level 10.	Hugo Herbelin	2017-11-27
* \|	Restrict universe context when declaring constants in obligations.	Gaëtan Gilbert	2017-11-25
* \|	Fix interpretation of global universes in univdecl constraints.	Gaëtan Gilbert	2017-11-25
* \|	In close_proof only check univ decls with the restricted context.	Gaëtan Gilbert	2017-11-24
* \|	restrict_universe_context: do not prune named universes.	Gaëtan Gilbert	2017-11-24
* \|	Stop exposing UState.universe_context and its Evd wrapper.	Gaëtan Gilbert	2017-11-24
\|/
*	Fixing factorization of recursive notations in the case of an atomic separator.	Hugo Herbelin	2017-11-20
*	Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...	Maxime Dénès	2017-11-20
\|\
\| *	One more step in fixing #5762 ("where" clause).	Hugo Herbelin	2017-11-14
* \|	Merge PR #922: New beta-iota compatibility refinements	Maxime Dénès	2017-11-08
\|\ \ \| \|/ \|/\|
* \|	Merge PR #1139: Add a linter.	Maxime Dénès	2017-11-06
\|\ \
\| * \|	Put newlines at the end of files.	Gaëtan Gilbert	2017-10-25
* \| \|	Moving bug numbers to BZ# format in the test-suite.	Théo Zimmermann	2017-10-19
* \| \|	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
\| \|/ / / \|/\| \| \|
\| \| \| *	Fixing another regression with 8.4 wrt to βι-normalization of created hyps.	Hugo Herbelin	2017-08-21
\| \| \| *	Fixing a new regresssion with 8.4 wrt to βι-normalization of created hyps.	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