aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
Commit message (Collapse)AuthorAge
* coqdep: honor dependencies of "Load"ed filesGravatar gareuselesinge2012-10-29
| | | | | | | | | | | | | Imagine A.v "Load"s B.v and that B.v "Require"s C. Before this commit we get: A.vo: A.v B.v After this commit we get: A.vo: A.v B.v C.vo git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15939 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow running coq-tex in win32 (fix #2921)Gravatar letouzey2012-10-29
| | | | | | | | | Yes, it seems that < and > and even 2>&1 are legal under windows :-) Btw, the only function using streams has been rewritten, so coq_tex is now a standard .ml file, not a .ml4 anymore (beware during upgrade!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15938 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r15885 fixing coqdoc index bugs introduced in r14624 and r15053.Gravatar herbelin2012-10-16
| | | | | | | Indeed r15885 still had problems (index contained referenced objects and not only defined objects, sorry). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15893 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed dead code about linking Module names in coqdoc.Gravatar herbelin2012-10-16
| | | | | | | Code was probably unused since scan_file made obsolete in r11024. See also r12890. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: easier compilation with timings info (from r15850)Gravatar pboutill2012-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15888 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing coqdoc index bugs introduced in r14624 and r15053. Revision r14624 ↵Gravatar pboutill2012-10-15
| | | | | | | | introduced bug #2709 on duplicate entries in index and tentative fix of it in r15053 mixed up names of files and names of constants in index (as reported by P. Castéran on coqdev). Patch by Hugo Herbelin :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15885 85f007b7-540e-0410-9357-904b9bb8a0f7
* fix r15860 : no slash after $(COQLIB)Gravatar letouzey2012-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15882 85f007b7-540e-0410-9357-904b9bb8a0f7
* still some more dead code removalGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove -rectypes except for term.mlGravatar letouzey2012-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" ;-)Gravatar letouzey2012-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 outputGravatar glondu2012-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 fixupsGravatar pboutill2012-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
* More type-safe interface to Coq XML API.Gravatar ppedrot2012-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15813 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-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,Gravatar regisgia2012-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
* Coqdoc: fix --utf8 bug for pretty printingGravatar pboutill2012-09-07
| | | | | | Author: Francois Ripault <francois.ripault@epita.fr> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15782 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more states/initial.coq, instead coqtop now requires Prelude.voGravatar letouzey2012-08-23
| | | | | | | | For starting a bare coqtop, the recommended option is now "-noinit" that skips the load of Prelude.vo. Option "-nois" is kept for compatibility, it is now an alias to "-noinit". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "when cross-compiling with mingw32, let's fix the Filename.dir_sep"Gravatar letouzey2012-08-23
| | | | | | | This was merely cosmetic after all, since recent Windows versions do tolerate paths with /. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15750 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdoc inlined verbatim_char in latexGravatar pboutill2012-08-06
| | | | | | Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15690 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add inline verbatim (<</>>), quotes (") and urls ({{url} name}) ↵Gravatar pboutill2012-08-06
| | | | | | markup/typesetting to coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15689 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdoc: More keywords, better special char escape, special case for "in *"Gravatar pboutill2012-08-05
| | | | | | Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15680 85f007b7-540e-0410-9357-904b9bb8a0f7
* More entries in the indexGravatar pboutill2012-08-05
| | | | | | Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15678 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various minor fixes to coqdoc from A. Chlipala.Gravatar msozeau2012-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15624 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed fake_ide test-suite.Gravatar ppedrot2012-07-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15564 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing fake_ideGravatar ppedrot2012-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15502 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: make uninstall targetGravatar pboutill2012-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15480 85f007b7-540e-0410-9357-904b9bb8a0f7
* Install is rather beautifulGravatar pboutill2012-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15479 85f007b7-540e-0410-9357-904b9bb8a0f7
* inthe middle one more timeGravatar pboutill2012-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15478 85f007b7-540e-0410-9357-904b9bb8a0f7
* Refactoring seems OKGravatar pboutill2012-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 ↵Gravatar pboutill2012-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 fixupGravatar pboutill2012-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_makefilesGravatar pboutill2012-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15435 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile bug for pluginsGravatar pboutill2012-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/Gravatar letouzey2012-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 contribsGravatar pboutill2012-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.cmaGravatar pboutill2012-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 85f007b7-540e-0410-9357-904b9bb8a0f7
* configure: add support of MinGW Win32 environment (fix #2526)Gravatar letouzey2012-05-23
| | | | | | | | | | | | | | * Since MinGW/Msys doesn't provide a cygpath utility, we emulate it via an ocaml script tools/mingwpath.ml * Avoid the crazy sed portions for backslash escaping, instead use a more robust ocaml script tools/escape_string.ml based on String.escaped * No more config/Makefile.template + sed on it, but rather a "cat << EOF > ..." as for config/coq_config.ml * Normally, support of Cygwin should be preserved, as well as mingw32 cross-compilation from linux (cf. myocamlbuild.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15348 85f007b7-540e-0410-9357-904b9bb8a0f7
* when cross-compiling with mingw32, let's fix the Filename.dir_sepGravatar letouzey2012-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15327 85f007b7-540e-0410-9357-904b9bb8a0f7
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
| | | | | | | | | | | | | | | - Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2709: Duplication in coqdoc index entriesGravatar pboutill2012-03-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15053 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: Add of extra options by defaultGravatar pboutill2012-02-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14997 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix handling of space after "Notation" or "where", add missing keywords.Gravatar msozeau2012-02-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14983 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdoc: Fixing missing newline when using "Proof term."Gravatar herbelin2011-12-26
| | | | | | | (bug apparently introduced by r11880). Fixing also a "body_bol" which apparently should be a "bol". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14866 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: "beautify" targetGravatar pboutill2011-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14809 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdep adds %.v.beautified on the left of the ':' when it generates %.v ↵Gravatar pboutill2011-12-17
| | | | | | dependecies. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14808 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: "validate" target calls the checker over all vo.Gravatar pboutill2011-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 ↵Gravatar pboutill2011-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 ↵Gravatar pboutill2011-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
* Added an API call to retrieve and change the option stateGravatar ppedrot2011-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14731 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 07:32:06 +0000