coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
*	Misc small fixes : warning, dep cycles, ocamlbuild...	letouzey	2010-04-26
\| \| \| \| \| \| \| \| \| \| \| \|	- git ignore g_decl_mode.ml - exhaustive match for pp_vernac (BeginSubproof, ...) - for ocamlbuild, remove a spurious cycle in recordops.mli (unnecessary open of Classops), and fixes of *.itargets and _tags The compilation via ocamlbuild still need some work, since plugin firstorder now depends on the new plugin decl_mode git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12964 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Win32 cross-compilation from debian: build of coqide.exe and other binaries	letouzey	2010-02-24
	Details will follow. In a word, we use a gtk+ win32 bundle from gtk.org to build some (unofficial) mingw32-liblablgtk2 debian packages. Then ./configure -local && ./build win32 is enough to get all native win32 binaries and plugin cmxs from a confortable linux box. Next step: an auto-installer :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12804 85f007b7-540e-0410-9357-904b9bb8a0f7