| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
"Context.Rel.Declaration.to_tuple" function"
This reverts commit 4b24bb7d3b770592015c264001b9aed9fe95c200.
While the of_tuple function is clearly dubious and mostly used for compatiblity reasons,
and thus had to be removed, I think that the to_tuple function is still useful as it
allows to access each component of the declaration piecewise. Without it, some codes
tend to get cluttered with useless projections here and there.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
Delimit the scope of the failure to ease potential need for debugging
the debugging printer.
Protect against one of the causes of failure (calling
get_family_sort_of with non-synchronized sigma).
|
| | | |
|
| | | |
|
| | | |
|
| | |\ |
|
| | |\ \ |
|
| | |\ \ \ |
|
| | |\ \ \ \
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
We used to recompute all fresh named contexts for evars before this patch in
the push_rel_context_to_named_context function. This was incurring a linear
penalty and a memory explosion due to the reallocation of many arrays. Now, we
rather remember the context between evar creations by sharing it in the pretyping
environment.
This can be considered as a fix for bug #4964 even though we might do better.
|
| | | | |\ \ \ |
|
| | | | |/ / /
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
In Coqide 8.5pl2, "forward one command" (down arrow) always repositions the insertion point at the end of the phrase being executed, just after the final ".".
In Coqide 8.4, the insertion point is not moved if it is after the end of the executed phrase. The insertion point is moved only if it falls behind the phrase being executed.
I find the 8.5 behavior to be a regression over the lot more useful 8.4 behavior. This commit restores the 8.4 behavior of "forward one command".
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
function
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
function
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
While the performance gain should go unnoticed in most cases, in some
degenerate situations, e.g. the evar-stressing test-case of bug #4964,
this commit speeds up coq by 10% since most of the time is spent scanning
long lists with most of the elements filtered out.
Note that this commit also changes the scanning order to front-to-back,
which is a bit less surprising (though no code should ever depend on the
scanning order).
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
This saves a quadratic allocation by replacing arrays with maps.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
In addition to sharing, we also delay the computation of the environment in
a by-need fashion.
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
We remove in particular a dubious use of an environment in fresh name
generation. The code was using the wrong environment in a function only
depending on the rel context which was resetted most of the time. This
might change the generated names in extremely rare occurences.
|
| | | | | | | |
|
| | |/ / / / |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
Modulo delta for types should be fully transparent.
|
| | |\| | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
Fixes both bugs #4924 and #4437.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This historical Makefile was used during the development of coqcheck,
but was unused since then : the checker is built via Coq's main Makefile.
So let's remove this one to avoid any risk of confusion.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This file was only used during ocamldebug sessions (in the dev/db
script). It was containing a large subset of the core cma files,
up to the printing functions. There were a few notable exceptions,
for instance no kernel/vm.cmo to avoid loading dllcoqrun.so in ocamldebug.
But printers.cma was troublesome to maintain : almost each time an ML file
was added/removed/renamed in the core of Coq, dev/printers.mllib
had to be edited, in addition to the directory-specific .mllib
(kernel/kernel.mllib and co). So I propose here to kill this file,
and put instead in dev/db several "load_printer" of the core cma files.
For that to work, we need to compile kernel/kernel.cma with the right
-dllib and -dllpath options, but that shouldn't hurt (on the contrary).
We also source now the camlpX cma in dev/db, via a new generated file
dev/camlp4.dbg containing a load_printer of either gramlib.cma or
camp4lib.cma.
If one doesn't want to perform the whole "source db" at the start
of an ocamldebug session, then the former "load_printer printers.cma"
could be replaced by:
source core.dbg
load_printer top_printers.cmo
See for instance the minimal dev/base_db.
|
| | | | | | |
|
| |\| | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Apparently, in camlp4 (unlike camlp5) :
- Something like "[ kwd = IDENT "foobar" -> .... kwd ... ]"
produces a kwd of type token instead of string (which sounds reasonable ?).
For now, I've replaced kwd by the explicit strings. Not so nice, but works
with both camlp4 and camlp5
- A quotation of the form "let obj = ... in bar; baz" is not
interpreted in the usual OCaml way, but rather as
"(let obj = ... in bar); baz".
Let's use instead "let obj = ... in let () = bar in baz", which works fine.
|
| | | | | | |
|
| | | |\ \ \ |
|
| | | |/ / /
| | | | |
| | | | |
| | | | |
| | | | | |
when checking that the rewrite relation is homogeneous in
setoid_rewrite.
|
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Hugo Herbelin
Guillaume Melquiond
Xavier Leroy
Matej Kosik
Matthieu Sozeau
Matthieu Sozeau
Pierre Letouzey