| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This reverts commit df69c44af03f2587b3f1706a805d0e2728c1f1dc.
Should be merged before any PR with plugin tutorial overlays, or we
can just merge the vendor PR instead.
|
|
|
|
|
|
|
|
We need to update in Docker:
- dune to 1.4.0: as it honors `-p` on test stanzas
- dune-release to 1.1.0: support for OPAM 2.0 + fixes
This makes `dune-release distrib` / `dune-release opam pkg` work.
TODO: we need to figure out what is going on with the
versioning. Should we do `dune subst` on `pinned`?
|
|
As noted by Gäetan, we didn't compile these. We also provide a recipe
to run `ocamldebug`. Try (after a build):
```
dune exec dev/dune-dbg
(ocd) source dune_db
```
or
```
dune exec dev/dune-dbg checker
(ocd) source checker_dune_db
```
for the checker.
|
|
We make `config` into a properly library. This is more uniform and
useful for some clients. This also matches what was done in Dune.
Next step would be to push dependencies on `Coq_config` upwards, only
the actual toplevel binaries should depend on it.
We also remove the stale `camlp5.dbg` and refactor the dbg files a
bit, isolating the bits that are specific to the plugin / lib building
method used by makefile.
|
|
This includes many changes, please have a look at the newly generated
docs.
|
|
|
|
This fixes the CI until this commit is merged into master.
|
|
We had a brief leftovers of the ocamlbuild experiment that are not
relevant anymore as it was removed from the tree a few years ago.
p.s: The amount of cruft we have in the `dev/build/windows` folder is
staggering, see for example what `git grep ocamlbuild` returns.
|
|
I'd like to add this convention as it is very convenient for the
development of dev tools. Example, I can do `setup-coq-devs ltac
equations` and then get a fully composed tree. Similarly for preparing
overlays.
|
|
|
|
Those optional arguments did not really make sense. It was pretty clear from
our code base, as all instances where triplicating the same type for TYPED,
RAW_TYPED and GLOB_TYPED.
|
|
|
|
Fixes #8337
|
|
Not a big point on running the checker on Appveyor I think, this will
save a bunch of time and improve reliability.
|
|
"Declaration" hooks can be polymorphic on their return type, however
this facility doesn't seem used in the codebase.
We thus remove the polymorphism with the hope to be able to reify the
control later on.
|
|
|
|
|
|
We refactor the `Coqlib` API to locate objects over a namespace
`module.object.property`.
This introduces the vernacular command `Register g as n` to expose the
Coq constant `g` under the name `n` (through the `register_ref`
function). The constant can then be dynamically located using the
`lib_ref` function.
Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org>
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
This satisfies a wish by @ppedrot
|
|
And fix a typo that was previously there.
|
|
|
|
|
|
|
|
|
|
A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This was broken due to a typo when introducing the archive download
method.
We also remove default [master] values from basic-overlay which hid
this issue.
|
|
We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code.
Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.
|
|
|
|
|
|
This was mostly a matter of adding backquotes and indentation where
needed. There were also some "combining grave accent" used in place of
proper backquotes.
I cleaned only the changes of the most recent releases.
|
|
The Dune `release` profile is used by OPAM so that should cover the
testing.
We also update the dependencies:
- camlp5: 7.01 had some bugs regarding grammar; we could use 7.02,
however this version it is not in OPAM. So I guess that leaves us
with 7.03 again.
- lablgtk < 2.18.5 does not support OCaml >= 4.05.0.
|
|
|
|
|
|
|
|
|
|
Implemented by merging addon changes in V8.8.2 (keeping everything on master)
|
|
|
|
Fixes #8621
|
|
compat updates to do as part of a release.
|
|
|
