coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Micromega clean-up	Maxime Dénès	2018-06-07
\| \| \| \| \| \| \| \| \|	We add .mli files, removed dead code and use standard combinators instead of redefined ad-hoc ones in a few places. A lot of cleaning still has to be done on this code: documenting the interfaces, resolving the many abstraction leaks. I suspect there is still a lot of code duplication.
*	Disambiguate Polynomial.Hyp and Mfourier.Hyp -> Assum	Gaetan Gilbert	2017-04-27
\|
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey	2016-07-03
\| \| \| \| \| \|	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
*	Fix typos.	Guillaume Melquiond	2016-01-01
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
\| \|
* \|	micromega : options to limit proof search	Frédéric Besson	2015-05-26
\|/
*	Correct a spelling mistake	Jason Gross	2014-08-25
\|
*	Fixing ml-doc.	Pierre-Marie Pédrot	2014-05-01
\|
*	Fixing some generic equalities in Micromega.	Pierre-Marie Pédrot	2014-03-03
\|
*	Fixing pervasive comparisons	Pierre-Marie Pédrot	2014-03-01
\|
*	Restrict (try...with...) to avoid catching critical exn (part 11)	letouzey	2013-03-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16287 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	the new Int module. Only the most obvious were removed, so there are a lot more in the wild. This may sound heavyweight, but it has two advantages: 1. Monomorphization is explicit, hence we do not miss particular optimizations of equality when doing it carelessly with the generic equality. 2. When we have removed all the generic equalities on integers, we will be able to write something like "let (=) = ()" to retrieve all its other uses (mostly faulty) spread throughout the code, statically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Improved lia + experimental nlia	fbesson	2011-05-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14116 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	micromega : Better parsing of formulae - smaller proof terms for Z - ↵	fbesson	2009-07-30
\| \| \| \| \| \|	redesign of proof cache git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12254 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵	letouzey	2009-03-20
	user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7