coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Moving argument-free tactics out of the AST into a dedicated	Pierre-Marie Pédrot	2014-05-16
\| \| \| \|	"coretactics.ml4" file.
*	Adding an interface to Eqdecide and putting the grammar rules in a dedicated	Pierre-Marie Pédrot	2014-03-26
\| \| \| \|	file.
*	Splitting Class_tactics between code and CAMLP4/5 declarations.	ppedrot	2013-10-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16847 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Splitting Rewrite into a code part and a CAMLP4-dependent one.	ppedrot	2013-09-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16804 85f007b7-540e-0410-9357-904b9bb8a0f7
*	No need to have Refine amongst Hightactics.cm*a	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15388 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Move setoid_rewrite to its own module and do some clean up in	msozeau	2009-04-07
\| \| \| \| \| \| \|	class_tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12056 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey	2009-03-20
	* generalize the use of .mllib to build all cma, not only in plugins/ * the .mllib in plugins/ now mention Bruno's new _mod.ml files * lots of .cmo enumerations in Makefile.common are removed, since they are now in .mllib * the list of .cmo/.cmi can be retreive via a shell script line, see for instance rule install-library * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not _files_ * a -I option to coqdep_boot allows to control piority of includes (some files with the same names in kernel and checker ...) This is quite a lot of changes, you know who to blame / report to if something breaks. ... and last but not least I've started playing with ocamlbuild. The myocamlbuild.ml is far from complete now, but it already allows to build coqtop.{opt,byte} here. See comments at the top of myocamlbuild.ml, and don't hesitate to contribute, either for completing or simplifying it ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7