coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Adding a timeout to bug #2447.	Pierre-Marie Pédrot	2014-10-15
*	Fix for bug #3618.	Matthieu Sozeau	2014-10-15
*	Bug 3692 is fixed.	Matthieu Sozeau	2014-10-15
*	Bug 3628 is fixed.	Matthieu Sozeau	2014-10-15
*	Add a bunch of reproduction files for bugs.	Xavier Clerc	2014-10-03
*	Add a bunch of reproduction files for bugs.	Xavier Clerc	2014-09-30
*	In evarconv and unification, expand folded primitive projections to	Matthieu Sozeau	2014-09-29
*	Keyed unification option, compiling the whole standard library	Matthieu Sozeau	2014-09-27
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Add a bunch of reproduction files for bugs.	Xavier Clerc	2014-09-26
*	Add missing "Fail" to bug cases.	Xavier Clerc	2014-09-26
*	Bug #3566 is fixed.	Xavier Clerc	2014-09-26
*	Add several reproduction files for bugs.	Xavier Clerc	2014-09-25
*	Update test-suite files.	Matthieu Sozeau	2014-09-24
*	Update test-suite files after last commit. Add a file for rewrite_strat	Matthieu Sozeau	2014-09-17
*	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau	2014-09-17
*	Fix test-suite files, and move some opened to closed.	Matthieu Sozeau	2014-09-11
*	Status error for bug #3459.	Pierre-Marie Pédrot	2014-09-04
*	Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible	Matthieu Sozeau	2014-08-25
*	Fix test-suite file.	Matthieu Sozeau	2014-08-18
*	Restrict eta-conversion to inductive records, fixing bug #3310.	Matthieu Sozeau	2014-08-14
*	Fix evarconv not applying eta when it used to. Fixes bug#3319.	Matthieu Sozeau	2014-08-08
*	Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl...	Matthieu Sozeau	2014-07-03
*	Indeed simpl never is really honored now.	Matthieu Sozeau	2014-07-02
*	Invalid bug report.	Matthieu Sozeau	2014-06-26
*	Fix bug # 3325 using canonical structure declarations where needed.	Matthieu Sozeau	2014-06-26
*	Add an option to disable typeclass resolution during conversion, which	Matthieu Sozeau	2014-06-26
*	Merge branch 'tc-test-suite' of https://github.com/JasonGross/coq into JasonG...	Matthieu Sozeau	2014-06-26
\|\
* \|	Fixed bug with new semantics of change.	Matthieu Sozeau	2014-06-26
* \|	Duplicate	Matthieu Sozeau	2014-06-26
* \|	This has been fixed.	Matthieu Sozeau	2014-06-26
* \|	Properly refresh the local hintdb database in case an external tactic changed	Matthieu Sozeau	2014-06-26
* \|	Fix test-suite file, adding the proper Fail.	Matthieu Sozeau	2014-06-26
* \|	Bug #3329 is closed.	Matthieu Sozeau	2014-06-26
* \|	3392 is now closed thanks to E. Tassi.	Matthieu Sozeau	2014-06-26
* \|	Merge branch 'more-test-suite' of https://github.com/JasonGross/coq into Jaso...	Matthieu Sozeau	2014-06-26
\|\ \
* \| \|	Fix test-suite files.	Matthieu Sozeau	2014-06-26
* \| \|	Bug #3301 is closed, the projection cannot be defined anymore.	Matthieu Sozeau	2014-06-26
* \| \|	Fix test-suite file for opened bug #1596	Matthieu Sozeau	2014-06-26
\| \| *	Update some bugs about typeclass resolution	Jason Gross	2014-06-24
\| \|/ \|/\|
* \|	Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)	Enrico Tassi	2014-06-23
\| *	More test-suite cases	Jason Gross	2014-06-22
\|/
*	- Add an option to refresh only algebraic universes, for e_type_of. The goal	Matthieu Sozeau	2014-06-21
*	Fixed bug 3332.	Matthieu Sozeau	2014-06-20
*	Allow more relaxed conversion between the types of the two terms of a rewrite	Matthieu Sozeau	2014-06-20
*	Fix computation of inductive level in monomorphism + indices-matter mode.	Matthieu Sozeau	2014-06-20
*	Fixed some HoTT bugs, provide a proper error message when giving an ill-formed	Matthieu Sozeau	2014-06-20
*	Bug 27 closed now that universe contexts can be refined during the proof,	Matthieu Sozeau	2014-06-20
*	HoTT coq bug #62 fixed.	Matthieu Sozeau	2014-06-19
*	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau	2014-06-18