coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Fixes the lost evars when interpreting a change with pattern tactic.	Arnaud Spiwack	2014-06-06
*	Remove the syntax [Vernac1. Vernac2. … Vernacn. ].	Arnaud Spiwack	2014-06-06
*	Make kernel reduction code parametric over the handling of universes,	Matthieu Sozeau	2014-06-06
*	Moving the [split] tactic out of the AST.	Pierre-Marie Pédrot	2014-06-06
*	Dedicated map module for type universes. It uses hashmaps, which are	Pierre-Marie Pédrot	2014-06-05
*	Removing dead code from Univ.	Pierre-Marie Pédrot	2014-06-05
*	Make standard library independent of the names generated by	Hugo Herbelin	2014-06-04
*	Make standard library independent of the names generated by	Hugo Herbelin	2014-06-04
*	Collecting in Namegen those conventional default names that are used in diffe...	Hugo Herbelin	2014-06-04
*	Small lemma about Relations.	Hugo Herbelin	2014-06-04
*	Remove spurious Show in script.	Matthieu Sozeau	2014-06-04
*	- Better parsing and printing of named universes: Type{ident} and foo@{(ident...	Matthieu Sozeau	2014-06-04
*	Fix canonical structure resolution (makes test-suite files go through again).	Matthieu Sozeau	2014-06-04