| Commit message (Collapse) | Author | Age |
|\ |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
|
|\ \ |
|
|\ \ \
| | | |
| | | |
| | | | |
implementation from Detyping.
|
|\ \ \ \ |
|
| | | | |
| | | | |
| | | | |
| | | | | |
Also adding fold_right_map by consistency.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Also renaming fold_map' into fold_right_map, and fold_map2' into
fold_right2_map.
|
| |_|/ /
|/| | |
| | | |
| | | |
| | | | |
- Adding fold_left2_map/fold_right2_map.
- Canonically renaming fold_map/fold_map' into fold_left_map/fold_right_map.
|
| | | | |
|
| |/ /
|/| |
| | |
| | | |
from Detyping.
|
| |/
|/| |
|
|\ \
| | |
| | |
| | | |
trailing / and \ on windows)
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
This refines e234f3ef. By the way, note that e234f3ef fixed #5391
(command line tools do not accept trailing "/" - or "\" - in windows).
|
| |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | | |
This is a second try at removing the hooks for the legacy xml export
system which can't currently be tested.
It is also not included in the API, so it should either be included in
it or this PR be applied.
|
| | | |
|
|\ \ \
| |/ /
|/| | |
|
| |/ |
|
|\ \
| | |
| | |
| | | |
flag is set.
|
| |/
|/| |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
Calling it only when there is something to profile, or when profiling
is explicitly required with the profile flags, so that profiling in
plugins is possible.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
No need to call Gc functions nor Unix timing functions when there is
nothing to report.
Moreover, PMP observed problems with these functions in the
debugger. PMP also reported that Gc.minor takes some noticeable time,
so no need to trigger some when unneeded.
|
|\ \ |
|
|\ \ \
| |_|/
|/| | |
|
| |/
|/|
| |
| | |
Fix bug introduced by a Haskell programmer.
|
|\ \
| | |
| | |
| | | |
rather than colors
|
| | |
| | |
| | |
| | |
| | | |
eval thunks once in prlist_sep_lastsep, make code clearer
add typeclass debug output test
|
| |/
| |
| |
| |
| |
| |
| |
| | |
This is usable for no-color terminal.
For instance, a typical application in mind is the Coq-generate names
marker which can be rendered with a color if the interface supports it
and a prefix "~" if the interface does not support colors.
|
|/ |
|
|\ |
|
| | |
|
| |
| |
| |
| |
| |
| | |
The status of a warning can now be set before the warning is declared
(typically by a plugin). However, I had to remove the "unknown warning"
warning.
|
|\ \ |
|
| | | |
|
|/ / |
|
|\ \ |
|
|\ \ \ |
|
| | | | |
|
| | | | |
|
| | | | |
|
| |/ /
|/| |
| | |
| | | |
versions.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Plugin-writers can now use:
-bypass-API
parameter with "coq_makefile".
The effect of that is that instead of
-I API
the plugin will be compiled with:
-I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
|
| | | |
|
|/ / |
|
|\ \ |
|
| | | |
|
|/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
|