coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Coq_makefile: fix cmx compilation when there are both ml and mllib	Pierre Boutillier	2014-07-07
\|
*	Fix Coq_makefile in presence of mlpack	Pierre Boutillier	2014-07-03
\|
*	Bug 3405: Coq_makefile: Implicit rules only for listed files in Make file	Pierre Boutillier	2014-07-03
\|
*	Coq_makefile takes advantages of -I -Q -R cleanup	Pierre Boutillier	2014-06-30
\|
*	Coq_makefile: -extra[-phony] correction + doc	Pierre Boutillier	2014-06-30
\|
*	coq_makefile: -I for the new stm/ dir	Enrico Tassi	2014-04-25
\|
*	Adapt coq_makefile build rules to new -R -I semantic	Pierre Boutillier	2014-04-09
\|
*	Fix compilation of coq and plugins using coq_makefile under cygwin	Enrico Tassi	2014-02-28
\| \| \| \| \| \| \| \| \|	Problems: - strip may not be "strip" but "i686-bla-strip", hence we ask ocamlc -config the value of "ranlinb" and replace ranlib by strip obtaining "i686-bla-strip" from "i686-bla-ranlib" - coq_makefile was not quoting the plugins/ paths - coq_makefile was quoting twice camlpX (the shell of cygwin was confused)
*	coq_makefile: new target vi2vo	Enrico Tassi	2014-02-26
\|
*	-schedule-vi-checking ported to spawn	Enrico Tassi	2014-01-26
\|
*	.vi files: .vo files without proofs	Enrico Tassi	2014-01-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	File format: The .vo file format changed: - after the magic number there are 3 segments. A segment is made of 3 components: bynary int, an ocaml value, a digest. The binary int is the position of the digest, so that one can skip the value without unmarshalling it - the first segment is the library, as before - the second segment is the STM task list - the third segment is the opaque table, as before A .vo file has a complete opaque table (all proof terms are there). A .vi file follows the same format of a .vo file, but some entries in the opaque table are missing. A proof task is stocked instead. Utilities: coqc: option -quick generates a .vi insted of a .vo coq_makefile: target quick to generate all .vi coqdep: generate deps for .vi files too votour: can browse .vi files too, the first question is which segment should be read coqchk: rejects .vi files
*	Coqdep always uses / as dir_sep	Pierre Boutillier	2013-12-20
\|
*	Getting rid of the use of deprecated elements (from the OCaml standard library).	xclerc	2013-10-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revert "remove -rectypes except for term.ml"	mdenes	2013-01-22
\| \| \| \| \| \| \| \| \| \|	Preparing landing of the native compiler, which requires -rectypes flag. This reverts commit f975575187d0a19e7cc1afc43459a92eeb12b3f1. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16135 85f007b7-540e-0410-9357-904b9bb8a0f7
*	I forget to use git log before git svn dcommit ...	pboutill	2013-01-18
\| \| \| \| \| \| \| \| \| \| \| \|	Revert "Revert "coq_makefile: use coqdep instead of ocamldep on .ml4 files"" This reverts commit 7b9856f2eae3bd652d99864c9901f7c4af290323. The reason for my private revert is that coqdep does not find the dependencies of .ml4 files in AACTactics user-contrib correctly but it is a coqdep bug not a coq_makefile one ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16131 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revert "coq_makefile: use coqdep instead of ocamldep on .ml4 files"	pboutill	2013-01-18
\| \| \| \| \| \|	This reverts commit d14b9f6a017347e59cf037ff576f282785105080. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16128 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: quoting paths	pboutill	2013-01-07
\| \| \| \| \| \| \| \|	Global paths (binaries & install dir) are quoted, local paths are never ! From a patch by Jason Gross. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16119 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: -extra & -phony-extra for user defined makefile rule	pboutill	2013-01-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16118 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: Better rule for subdirs when the subdir does not exist	pboutill	2012-12-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16056 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revert "* tools/Coq_makefile:"	regisgia	2012-12-07
\| \| \| \| \| \|	This reverts commit 9a2f43eca179436f0581751b93c989fd30a5c13c. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16029 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* tools/Coq_makefile	regisgia	2012-12-07
\| \| \| \| \| \|	Export $(COQMKTOP) in generated Makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16028 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* tools/Coq_makefile:	regisgia	2012-12-07
\| \| \| \| \| \| \|	Add '-I config' in the options of the ocaml compilers. This is useful to reuse site configuration in plugins. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16027 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq_makefile: use coqdep instead of ocamldep on .ml4 files	gareuselesinge	2012-11-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15967 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: easier compilation with timings info (from r15850)	pboutill	2012-10-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15888 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fix r15860 : no slash after $(COQLIB)	letouzey	2012-10-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15882 85f007b7-540e-0410-9357-904b9bb8a0f7
*	remove -rectypes except for term.ml	letouzey	2012-10-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15871 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Repair the configure after Hugo's last "repair" ;-)	letouzey	2012-10-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Ok, I wasn't aware of the funny behavior of cd in presence of $CDPATH. But the last "repair" was worse, trying to write into non-existing file theories/config/coq_config.ml Things should be better now: * no more Coq_config.theories_dirs at all, since it was completely unused :-) * concerning Coq_config.plugins_dirs, we list them without any "cd" into plugins, hence keeping the "plugins/" part in their paths, and adapt accordingly the only use (!) of plugins_dirs, in coq_makefile Please run ./configure again after upgrading to this commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15860 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix use of $(HASNATDYNLINK) in coq_makefile output	glondu	2012-09-22
\| \| \| \| \| \| \| \|	Generated makefiles were broken because $(if ifeq '$(HASNATDYNLINK)' 'true',X) always returns X. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15826 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile fixups	pboutill	2012-09-18
\| \| \| \| \| \| \|	- put %.cmxs rule from %.cmxa before the one from %.cmx. - erase \r in included output of commands for windows git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15820 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
\| \| \| \| \| \| \| \| \|	List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	especially about unused definitions, unused opens and unused rec flags. The following patch uses information gathered using these warnings to clean Coq source tree. In this patch, I focused on warnings whose fix are very unlikely to introduce bugs. (a) "unused rec flags". They cannot change the semantics of the program but only allow the inliner to do a better job. (b) "unused type definitions". I only removed type definitions that were given to functors that do not require them. Some type definitions were used as documentation to obtain better error messages, but were not ascribed to any definition. I superficially mentioned them in one arbitrary chosen definition to remove the warning. This is unaesthetic but I did not find a better way. (c) "unused for loop index". The following idiom of imperative programming is used at several places: "for i = 1 to n do that_side_effect () done". I replaced "i" with "_i" to remove the warning... but, there is a combinator named "Util.repeat" that would only cost us a function call while improving readibility. Should'nt we use it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: make uninstall target	pboutill	2012-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15480 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Install is rather beautiful	pboutill	2012-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15479 85f007b7-540e-0410-9357-904b9bb8a0f7
*	inthe middle one more time	pboutill	2012-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15478 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Refactoring seems OK	pboutill	2012-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15477 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: separate finding what to install where from generating the ↵	pboutill	2012-06-22
\| \| \| \| \| \|	script that install git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15476 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq_makefile fixup	pboutill	2012-06-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15438 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New step in purpose to get both camlp4 and camlp5 compatible coq_makefiles	pboutill	2012-06-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15435 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile bug for plugins	pboutill	2012-05-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15405 85f007b7-540e-0410-9357-904b9bb8a0f7
*	place all pretty-printing files in new dir printing/	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bugs revealed by playing with contribs	pboutill	2012-05-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15364 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revert copy/pasted function in to minilib thanks to clib.cma	pboutill	2012-05-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: Add of extra options by default	pboutill	2012-02-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14997 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: "beautify" target	pboutill	2011-12-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14809 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: "validate" target calls the checker over all vo.	pboutill	2011-12-17
\| \| \| \| \| \|	It uses short names so clashes can occur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14807 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: section refactoring and no variables for OCaml if no ml* files ↵	pboutill	2011-12-17
\| \| \| \| \| \|	in the generated code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14806 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: if no -install is provided, install location is set by a ↵	pboutill	2011-12-17
\| \| \| \| \| \| \| \| \| \|	Makefile variable or a special target. 1/ defining the USERINSTALL variable make a "user" installation instead of a "global" one. 2/ make userinstall is an alias for make USERINSTALL=true install git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14805 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Teach coq_makefile how to install into XDG_DATA_HOME.	pboutill	2011-11-20
\| \| \| \| \| \|	From Tom Prince. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14693 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq_makefile: Don't install with +x.	pboutill	2011-11-20
\| \| \| \| \| \|	By Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14691 85f007b7-540e-0410-9357-904b9bb8a0f7