coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Revert "syntax for exponents"	glondu	2011-02-25
\| \| \| \| \| \| \| \|	This reverts pottier's commit r13849. It references a ncring_plugin.cma for which there is no rule. I guess he forgot to commit something... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13856 85f007b7-540e-0410-9357-904b9bb8a0f7
*	syntax for exponents	pottier	2011-02-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13849 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Misc fixes related to new nsatz (and ocamlbuild)	letouzey	2010-06-03
\| \| \| \| \| \| \| \| \|	- Kill a warning in ideal.ml corresponding to really brain-dead code. - Restore extraction/vo.otarget in pluginsvo.itarget - In fact, plugins/_tags can be merged into _tags with nice ** patterns - Update .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13062 85f007b7-540e-0410-9357-904b9bb8a0f7
*	plugin groebner updated and renamed as nsatz; first version of the doc of ↵	pottier	2010-06-03
\| \| \| \| \| \|	nsatz in the refman git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13056 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extraction: start of a support library	letouzey	2010-06-02
\| \| \| \| \| \| \| \| \| \| \| \|	- ExtrOcamlBasic: mapping of basic types to ocaml's ones - ExtrOcamlIntConv: conversion between int and coq's numerical types - ExtrOcamlBigIntConv: same with big_int (no overflow) - ExtrOcamlNatInt: realizes nat by int (unsafe) more to come: Haskell, handling of stings, more stuff in ExtrOcamlNatInt, etc etc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13050 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Factorisation between Makefile and ocamlbuild systems : .vo to compile are ↵	letouzey	2009-12-09
\| \| \| \| \| \| \| \| \| \| \| \|	in //vo.itarget On the way: no more -fsets (yes\|no) and -reals (yes\|no) option of configure if you want a partial build, make a specific rule such as theories-light Beware: these vo.itarget should not contain comments. Even if this is legal for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix the build of coq via ocamlbuild	letouzey	2009-12-08
\| \| \| \| \| \| \| \|	- no more plugins/interface - a few missing files in theories.itarget - a few things required Unix now git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12572 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ocamlbuild: improvements suggested by N. Pouillard	letouzey	2009-04-03
	* Import of Coq_config via myocamlbuild_config.ml, instead of my get_env * As a consequence, we enrich this Coq_config with stuff that was only in config/Makefile * replace the big ugly find by some dependencies against source files * by the way: build csdpcert, with the right aliases. I've tried to escape things properly for windows in ./configure, but this isn't fully tested yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12046 85f007b7-540e-0410-9357-904b9bb8a0f7