| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
This reverts commit d14b9f6a017347e59cf037ff576f282785105080.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16128 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16118 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16056 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
This reverts commit 9a2f43eca179436f0581751b93c989fd30a5c13c.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16029 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Export $(COQMKTOP) in generated Makefiles.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16028 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15967 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15888 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15882 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15871 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
| |
- 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
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15480 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15479 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15478 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15477 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
script that install
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15476 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15438 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15435 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15405 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15364 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14997 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14809 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
in the generated code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14806 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
From Tom Prince.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14693 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
By Tom Prince
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14691 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
paths.
By Tom Prince
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14690 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14617 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Make the compilation log cleaner.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14609 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14608 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14599 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
a cmx?a
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14598 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Files in a -I path are now installed in every root directory of -R pathes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14445 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14443 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14434 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14433 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2334 85f007b7-540e-0410-9357-904b9bb8a0f7
|