| Commit message (Collapse) | Author | Age |
|\ |
|
|\ \ |
|
|\ \ \
| | | |
| | | |
| | | | |
camlp4
|
|\ \ \ \ |
|
| | | | |
| | | | |
| | | | |
| | | | | |
longer use camlp4.
|
| |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | | |
We organize the toplevel execution as a record and pass it
around. This will be used by future PRs as to for example decouple
goal printing from the classifier.
|
| | | |
| | | |
| | | |
| | | | |
(and alist-alist)
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
In current code, `Proofview.Goal.t` uses a phantom type to indicate
whether the goal was properly substituted wrt current `evar_map` or
not.
After the introduction of `EConstr`, this distinction should have
become unnecessary, thus we remove the phantom parameter from
`'a Proofview.Goal.t`. This may introduce some minor incompatibilities
at the typing level. Code-wise, things should remain the same.
We thus deprecate `assume`. In a next commit, we will remove
normalization as much as possible from the code.
|
|\ \ \ \
| |_|_|/
|/| | | |
|
|\ \ \ \ |
|
|\ \ \ \ \
| |_|_|_|/
|/| | | | |
|
| | | | | |
|
| | | | | |
|
| |/ / /
|/| | | |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
| |_|/ / /
|/| | | | |
|
|\ \ \ \ \ |
|
| |_|/ / /
|/| | | |
| | | | |
| | | | | |
Following comment at https://github.com/coq/coq/pull/6596#issuecomment-358246528.
|
| | | | | |
|
|\ \ \ \ \
| |_|/ / /
|/| | | | |
|
| |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We allow to provide a Coq load path at document creation time. This is
natural as the document naming process is sensible to a particular
load path, thus clarifying this API point.
The changes are minimal, as #6663 did most of the work here. The only
point of interest is that we have split the initial load path into two
components:
- a ML-only load path that is used to locate "plugable" toplevels.
- the normal loadpath that includes `theories` and `user-contrib`,
command line options, etc...
|
| | | | |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
menhir.
|
|\ \ \ \ \ |
|
| | |/ / / |
|
| | | | | |
|
|\ \ \ \ \ |
|
| | |/ / /
| |/| | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We separate functions dealing with VM values (vmvalues.ml) and
interfaces of the bytecode interpreter (vm.ml). Only the former relies
on untyped constructions.
This also makes the VM architecture closer to the one of native_compute,
another patch could probably try to share more code between the two for
conversion and reification (not trivial, though).
This is also preliminary work for integers and arrays.
|
|/ / / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Script modified from
https://unix.stackexchange.com/questions/175146/apt-get-update-exit-status
I stuck the code in "install" rather than "before_install" so that the
lint target didn't need to be changed. I also haven't touched the
targets that add more packages; I'll leave that to someone who knows
more about the "&" and "*" syntax being used in the configuration.
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
| | | | | | |
|
|\ \ \ \ \ \
| |_|/ / / /
|/| | | | | |
|
|\ \ \ \ \ \ |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
We inline should-check-whitespace.sh in check-eof-newline.sh
simplifying the find invocation.
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Since 5ffa147, there is a new clib folder that needed to be added to the set
of includes of ocamldebug
|
|\ \ \ \ \ \ \ |
|
| | | | | | | | |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \
| |_|/ / / / / / /
|/| | | | | | | | |
|
| |_|_|_|_|_|/ /
|/| | | | | | | |
|
| | | | | |/ / |
|
| | | | |/ /
| | | | | |
| | | | | |
| | | | | | |
Debian stable version is 0.42-3 right now.
|