coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Deprecate options -dont, -lazy, -force-load-proofs.	Guillaume Melquiond	2014-06-13
*	Less ocaml warnings.	Hugo Herbelin	2014-06-13
*	Improving tclWITHHOLES which did not see undefined evars up to	Hugo Herbelin	2014-06-13
*	Fixing "clear" in internal_cut_replace: forbid dependencies in the	Hugo Herbelin	2014-06-13
*	Improved error message when a meta posed as an evar remains unsolved	Hugo Herbelin	2014-06-13
*	Check resolution of Metas turned into Evars by pose_all_metas_as_evars	Hugo Herbelin	2014-06-13
*	Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).	Hugo Herbelin	2014-06-13
*	Adapt simpl/cbn unfolding and refolding machinery to projections, so that	Matthieu Sozeau	2014-06-13
*	Code cleaning in Univ.	Pierre-Marie Pédrot	2014-06-12
*	Passing some tactics to the new monad type.	Pierre-Marie Pédrot	2014-06-12
*	Fix bug #3291, stack overflow in rewrite.	Matthieu Sozeau	2014-06-11
*	Fix bug #3289	Matthieu Sozeau	2014-06-11
*	Move bug # 3368 to closed bugs	Matthieu Sozeau	2014-06-11
*	Merge branch 'more-test-suite' of https://github.com/JasonGross/coq into trunk	Matthieu Sozeau	2014-06-11
\|\
* \|	- Fix bug #3368, due to wrong use of the Cst_stack for projections.	Matthieu Sozeau	2014-06-11
* \|	In generalized rewrite, avoid retyping completely and constantly the conclusi...	Matthieu Sozeau	2014-06-11
* \|	fix handling of side effects in abstract (fixes QArithSternBrocot)	Enrico Tassi	2014-06-11
\| *	Add many more cases to the test-suite	Jason Gross	2014-06-10
\| *	Move closed bug 3314	Jason Gross	2014-06-10
\| *	Add a test-case for bug #3314 proving False	Jason Gross	2014-06-10
\|/
*	Fixing Sorting Universes in a world where le and lt constraints may be	Pierre-Marie Pédrot	2014-06-10
*	Compute the trace of a universe inconsistency only when explicitly required	Pierre-Marie Pédrot	2014-06-10
*	Made explanations for universe inconsistencies optional. They are only used	Pierre-Marie Pédrot	2014-06-10
*	Specialize the type of [Univ.compare_neq] so that it is clear it is only used	Pierre-Marie Pédrot	2014-06-10
*	Removing dead code in checker/univ.ml.	Pierre-Marie Pédrot	2014-06-10
*	Removing explanations of universe inconsistencies from the checker. They	Pierre-Marie Pédrot	2014-06-10
*	Imperatively check touched universes in compare_neq functions. This ensures	Pierre-Marie Pédrot	2014-06-10
*	Providing the checker with its own version of the Univ file.	Pierre-Marie Pédrot	2014-06-10
*	- Fix substitution of universes which needlessly hashconsed existing universes.	Matthieu Sozeau	2014-06-10
*	Oops, one refactoring was not compiled.	Matthieu Sozeau	2014-06-10
*	More cleanup/reorganizing of univ.ml to separate constraint/universe handling...	Matthieu Sozeau	2014-06-10
*	Fix module order in printers.mllib	Matthieu Sozeau	2014-06-10
*	Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...	Matthieu Sozeau	2014-06-10
*	Remove unused function in univ	Matthieu Sozeau	2014-06-10
*	Merge branch 'hott-test-suite-progress' of https://github.com/JasonGross/coq ...	Matthieu Sozeau	2014-06-10
\|\
* \|	Flattening Level module structure in Univ.	Pierre-Marie Pédrot	2014-06-09
\| *	Mark some progress in the HoTT/coq test-suite	Jason Gross	2014-06-08
* \|	Adding a toplevel option allowing to deactivate the term sharing in kernel	Pierre-Marie Pédrot	2014-06-08
\|/
*	Moving hook code from Future to Lemmas. This seemed to disrupt compilation of	Pierre-Marie Pédrot	2014-06-08
*	Fix canonical structure resolution in unification (bug found in Ssreflect).	Matthieu Sozeau	2014-06-08
*	Timeout implementation for Windows based on threads.	Pierre-Marie Pédrot	2014-06-08
*	Enforce a correct exception handling in declaration_hooks	Enrico Tassi	2014-06-08
*	ind_tables: always declare side effects (Closes: HOTT#110)	Enrico Tassi	2014-06-08
*	STM: handle "Time Abort" correctly (Closes: 3332)	Enrico Tassi	2014-06-08
*	Function in Univ uselessly exported.	Pierre-Marie Pédrot	2014-06-08
*	Removing 'open Univ' from checker.	Pierre-Marie Pédrot	2014-06-07
*	Moving a Thread.yield in check_interrupt.	Pierre-Marie Pédrot	2014-06-07
*	Adding a new Control file centralizing the control options of Coq.	Pierre-Marie Pédrot	2014-06-07
*	Preserve compatibility on examples such as "intros []." on goals such	Hugo Herbelin	2014-06-06
*	Dead code.	Hugo Herbelin	2014-06-06