coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
* \| \|	Fix test-suite file for bug # 3036, the unification has _never_ succeeded,	Matthieu Sozeau	2014-06-26
* \| \|	Change interface of refresh universes to get a pbty argument instead of	Matthieu Sozeau	2014-06-26
* \| \|	Add an Unset Standard...	Matthieu Sozeau	2014-06-26
* \| \|	Putting implicit arguments of Clenv.res_pf right.	Pierre-Marie Pédrot	2014-06-25
* \| \|	Incorrect folding of evars in let_tac_gen made remember fail to store	Matthieu Sozeau	2014-06-25
* \| \|	In rewrite, wrong computation of the sort of the term to be rewritten in	Matthieu Sozeau	2014-06-25
* \| \|	all coqide specific files moved into ide/	Enrico Tassi	2014-06-25
* \| \|	cut toploop(s) out of coqtop: now they are loaded dynamically	Enrico Tassi	2014-06-25
* \| \|	In exact check, use e_type_of to ensure that universe constraints necessary	Matthieu Sozeau	2014-06-25
* \| \|	Use the right transparent state when comparing _types_ of metas.	Matthieu Sozeau	2014-06-25
* \| \|	Fix type_of_inductive_knowing_conclusion, relying on an actually broken univ_...	Matthieu Sozeau	2014-06-25
* \| \|	Use full transparent state when checking well-typedness of a second order mat...	Matthieu Sozeau	2014-06-25
* \| \|	Fix computation of Type argument for Program's fix_proto.	Matthieu Sozeau	2014-06-24
* \| \|	Fix program cases and inversion tactic to correctly record universe constraints.	Matthieu Sozeau	2014-06-24
* \| \|	Force the final universe context of a proof only in poly \|\| now case.	Matthieu Sozeau	2014-06-24
\| \| *	Update some bugs about typeclass resolution	Jason Gross	2014-06-24
\| \|/ \|/\|
* \|	Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it	Pierre-Marie Pédrot	2014-06-24
* \|	Clenvtac.res_pf is in the new tactic monad.	Pierre-Marie Pédrot	2014-06-24
* \|	Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)	Enrico Tassi	2014-06-23
* \|	Add some compatibility notes on the changes to [change] and unification in ge...	Matthieu Sozeau	2014-06-23
* \|	Fix for bug 1951, allowing at least fully-applied inductives types to be used	Matthieu Sozeau	2014-06-23
* \|	Fix test-suite script for subst working with let-ins, the following proof was...	Matthieu Sozeau	2014-06-23
* \|	Changed syntax of explicit universes.	Matthieu Sozeau	2014-06-23
* \|	Clenvtac.unify is in the new monad.	Pierre-Marie Pédrot	2014-06-23
* \|	Removing opens to Clenvtac to track its use more easily.	Pierre-Marie Pédrot	2014-06-23
* \|	Oops, I fixed the .ml's	Matthieu Sozeau	2014-06-23
* \|	Fix semantics of change p with c to typecheck c at each specific occurrence o...	Matthieu Sozeau	2014-06-23
* \|	Proper handling of the polymorphism flag for Context, fixing HoTT bug #98.	Matthieu Sozeau	2014-06-23
* \|	The uses of the funext axiom forced levels to Set, relaxing its use doesn't.	Matthieu Sozeau	2014-06-23
* \|	The test-suite file couldn't typecheck as it rightly introduces a universe in...	Matthieu Sozeau	2014-06-23
* \|	Fix test-suite script for HoTT coq bug #34	Matthieu Sozeau	2014-06-23
\| *	More test-suite cases	Jason Gross	2014-06-22
\|/
*	Less goal-entering.	Pierre-Marie Pédrot	2014-06-22
*	Fixing grammar in doc of Opaque as proposed by Jason (#3389).	Hugo Herbelin	2014-06-21
*	Fixing #3390 (mismatch simple_tactic/tactic0 leading to segfault).	Hugo Herbelin	2014-06-21
*	Less ocaml warnings.	Hugo Herbelin	2014-06-21
*	- Add an option to refresh only algebraic universes, for e_type_of. The goal	Matthieu Sozeau	2014-06-21
*	When discharging polymorphic definitions, we must take into account all	Matthieu Sozeau	2014-06-21