| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.
Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.
If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.
Failure to precompile is a hard error, since it is now explicitly required
by the user.
|
|
|
|
The command [Redirect "filename" (...)] redirects all the output of
[(...)] to file "filename.out". This is useful for storing the results of
an [Eval compute], for redirecting the results of a large search, for
automatically generating traces of interesting developments, and so on.
|
|
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
|
|
|
|
Was made incorrect by 98a710caf5e907344329ee9e9f7b5fd87c50836f .
|
|
as glued.
Possible improvement: rotate using the left children in the glue function,
so that the iter function becomes mostly tail-recursive. Drawback: two
allocations per glue instead of a single one.
This commit makes the following command go from 7.9s to 3.0s:
coqtop <<< "Require Import BigZ ZBinary Reals OrdersEx. Time SearchPattern _." | tail -n 1
|
|
|
|
|
|
|
|
|
|
|
|
[kind_of_term].
To be able to write equality up to evar instantiation instantiation.
Generalises the main function of [eq] constr over the variant of [kind_of_term] it uses. It prevents some optimisation of [Array.equal] where two physically equal arrays are considered (less or) equal. But it does not seem to have appreciable effects on efficiency.
|
|
|
|
|
|
|
|
|
|
In particular:
- abstracting the code using calls to Unix opendir, stat, and closedir,
- uniformly using warnings when a directory does not exist (coqtop was
ignoring silently and coqdep was exiting via handle_unix_error),
- uniformly expecting paths in Unix format and warning otherwise.
|
|
(Sorry, was not intended to be pushed)
This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
|
|
In particular:
- abstracting the code using calls to Unix opendir, stat, and closedir,
- uniformly using warnings when a directory does not exist (coqtop was
ignoring silently and coqdep was exiting via handle_unix_error).
|
|
|
|
|
