coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to ↵	Matej Košík	2017-06-12
\| \| \| \|	generate them later.
*	extract "plugins/micromega/micromega.ml{,i}" files from ↵	Matej Kosik	2017-06-01
\| \| \| \|	"plugins/micromega/MExtraction.v"
*	micromega : more robust generation of proof terms	Frédéric Besson	2016-09-07
\| \| \| \| \| \| \|	- Assert a purely arihtmetic sub-goal that is proved independently by reflexion. (This reduces the stress on the conversion test) - Does not use 'abstract' anymore (more natural proof-term) - Fix a parsing bug (certain terms in Prop where not recognized)
*	added support to handle division by a constant over R	fbesson	2011-05-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14147 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
*	micromega: better handling of exponentiation + correction of test-suite ↵	fbesson	2009-09-18
\| \| \| \| \| \|	termination bug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12346 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
*	Micromega: improvement of the code obtained by extraction	letouzey	2009-03-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* In eval_cone and simpl_cone, default patterns were leading to duplicated computations. Adaptation of RingMicromega.v to prevent that. * Use the Ocaml builtin types (lists, pairs, bool, etc) and remove the useless conversion functions in mutils.ml and alii. * andb was extracted to a correctly lazy but ugly match. Let's rather use Ocaml's (&&). Remain to be done: take advantage of extraction during the build, - either directly if we are using plugins, (no dependency issues) - or if we compile statically, at least check later that the micromega.ml in the archive and the one auto-generated are in sync. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12034 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