| Commit message (Collapse) | Author | Age |
|\ |
|
| | |
|
| | |
|
|\| |
|
| | |
|
| | |
|
|\| |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
According to http://caml.inria.fr/mantis/view.php?id=5325
you can't use the same socket for both writing and reading.
The result is lockups (may be fixed in 4.03).
|
| | |
|
|\| |
|
| |
| |
| |
| | |
So that they display in response buffer.
|
| |
| |
| |
| |
| |
| | |
There is no reason (any longer?) to create simultaneous closures for
interning and externing files. This patch makes the code more readable
by separating both functions and their signatures.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
in the loadpath.
This patch causes a bit of code duplication (because of the .coq suffix
added to state files) but it makes it clear which part of the code is
looking up files in the loadpath and for what purpose. Also it makes the
interface of System.extern_intern and System.raw_extern_intern much saner.
|
|\| |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
and "Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that files"
and "Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X."
This reverts commits 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606
and 69941d4e195650bf59285b897c14d6287defea0f
and e7043eec55085f4101bfb126d8829de6f6086c5a.
Trying to emulate a case sensitive file system on top of a case aware one is
too costly: 3x slowdown when compiling the stdlib or CompCert.
|
|\| |
|
| | |
|
| | |
|
|\| |
|
| |
| |
| |
| |
| | |
Correcting the code w.r.t. to the API was not the right solution. Instead,
the API comment had to be corrected.
|
| |
| |
| |
| |
| |
| | |
We ensure statically by typing that the tags used by the rich printer
are integers. Furthermore, we also expose through typing that tags are
irrelevants in the returned XML.
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
Contrarily to what was described in the API, nodes without annotations
were not ignored by the printer but left there instead.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
| |
| |
| |
| |
| | |
hash-consing, so as to avoid having too many kinds of equalities with
same name.
|
|\| |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| | |
File system.ml seemed like a better choice than util.ml for sharing the
code, but it was bringing a bunch of useless dependencies to the IDE.
There are presumably several other tools that would benefit from using
open_utf8_file_in instead of open_in, e.g. coqdoc.
|
| |
| |
| |
| | |
This allows fatal_error to be used for printing anomalies at loading time.
|
|\| |
|
| |
| |
| |
| | |
This allows fatal_error to be used for printing anomalies at loading time.
|
| |
| |
| |
| |
| | |
Prints the VM bytecode produced by compilation of a constant or a call to
vm_compute.
|
| | |
|
| |
| |
| |
| |
| | |
Nothing is done for camlp4
There is an issue with computing camlbindir
|
|\| |
|
| |
| |
| |
| |
| |
| |
| | |
Of course there is an exception to the previous commit.
Fail used to print even if silenced but loading a vernac file.
This behavior is useful only in tests, hence this flag.
|
| |
| |
| |
| | |
Thanks to Vadim Zaliva for testing.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Fixed #4241 correlates Printing Width and max_indent, this patch
changes the correlation to the following one:
max_indent = max ((wdth*80)/100) (wdth-30)
i.e. the right column defined by max_indent is 20% of the global
width, but capped to 30 characters.
|
| |
| |
| |
| | |
when printing width extend).
|
| |
| |
| |
| |
| | |
found in the file system have the expected lowercase/uppercase
spelling)
|
| | |
|
| |
| |
| |
| |
| | |
expected lowercase/uppercase spelling (based on a patch by Pierre B.).
This should fix #2554 (and see also discussion on coq-club, May 2015).
|
|\|
| |
| |
| |
| |
| |
| | |
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
|
| | |
|
| |
| |
| |
| |
| |
| |
| | |
For now, warnings are still ignored by default, but this may change. This
commit at least allows to print them whenever desired. The -w syntax is
also opened to future additions to further control the display of
warnings.
|