| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
- We update the OCaml version used in the base CI image.
- Windows / OSX image building is also updated to use newer OCaml.
- We also update Dune to 1.0.0.
|
| |\ |
|
| | | |
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
| |
We deprecate the corresponding functions in Pcoq.Gram. The motivation is
that the Gram module is used as an argument to Camlp5 functors, so that
it is not stable by extension. Enforcing that its type is literally the
one Camlp5 expects ensures robustness to extension statically.
Some really internal functions have been bluntly removed. It is unlikely
that they are used by external plugins.
|
| |\ |
|
| | | |
|
| |/
|
|
|
|
|
|
|
| |
- move `README` to `README.md` to take advantage of markdown features
- remove `setup.txt`, port the editor specific information to the wiki.
Merge development information into `dev/doc/README.md`.
Wiki merge link: https://github.com/coq/coq/wiki/DevelSetup.
- Add new links to files into `dev/README.md`.
- Remove stale `translate.txt`.
|
| |\
| |
| |
| | |
points of Camlp5
|
| |\ \
| | |
| | |
| | | |
Z into three files
|
| | |/
|/| |
|
| |\ \ |
|
| | | | |
|
| |\ \ \
| |_|/
|/| |
| | | |
constr in Constr
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This shall eventually allow to use contexts of declarations in the
definition of the "Case" constructor.
Basically, this means that Constr now includes Context and that the
"t" types of Context which were specialized on constr are not defined
in Constr (unfortunately using a heavy boilerplate).
|
| | |/ |
|
| |/
|
|
| |
Both reminded by Enrico.
|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| | |
I let open several questions about fixes to the kernel which maybe
were not critical.
I skipped what seemed to have been bugs in beta-releases.
Need double-checks, decision about the format, etc.
|
| | |
| |
| |
| | |
[ci skip]
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We had mostly used absolute links in the past.
I just discovered that GitHub recommends using relative links instead:
https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links
and indeed my Emacs Markdown mode can handle relative links but doesn't
interpret absolute links relatively to the root of the git repository.
[ci skip]
|
| |/
|
|
|
| |
Bumping to 4.02.3 was decided some time ago in the WG, however a
couple of places escaped updating.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Continuing the interface cleanup we place `Constrexpr` in the
internalization module, which is the one that eliminates it.
This slims down `pretyping` considerably, including removing the
`Univdecls` module which existed only due to bad dependency ordering
in the first place. Thanks to @ Skyskimmer we also remove a duplicate
`univ_decl` definition among `Misctypes` and `UState`.
This is mostly a proof of concept yet as it depends on quite a few
patches of the tree. For sure some tweaks will be necessary, but it
should be good for review now.
IMO the tree is now in a state where we can could easy eliminate more
than 10 modules without any impact, IMHO this is a net saving API-wise
and would help people to understand the structure of the code better.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We make the vernacular implementation self-contained in the `vernac/`
directory. To this extent we relocate the parser, printer, and AST to
the `vernac/` directory, and move a couple of hint-related types to
`Hints`, where they do indeed belong.
IMO this makes the code easier to understand, and provides a better
modularity of the codebase as now all things under `tactics` have 0
knowledge about vernaculars.
The vernacular extension machinery has also been moved to `vernac/`,
this will help when #6171 [proof state cleanup] is completed along
with a stronger typing for vernacular interpretation that can
distinguish different types of effects vernacular commands can perform.
This PR introduces some very minor source-level incompatibilities due
to a different module layering [thus deprecating is not
possible]. Impact should be relatively minor.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | |_|/
|/| | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
comments.
[ci skip]
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Clarification prompted by Jim Fehrle.
[ci skip]
|
| |/ / |
|
| |\ \ |
|
| | |/
|/|
| |
| |
| |
| | |
This process is expected to evolve in the future as we automate it more and more.
[ci skip]
|
| | | |
|
| | |
| |
| | |
Simpler
|
| | |
| |
| | |
Actually there are more general instructions
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
|
|
|
| |
We move syntax for universes from `Misctypes` to `Glob_term`. There is
basically no reason that this type is there instead of the proper
file, as witnessed by the diff.
Unfortunately the change is not compatible due to moving a type to a
higher level in the hierarchy, but we expect few problems.
This change plus the related PR (#6515) moving universe declaration to
their proper place make `Misctypes` into basically an empty file save
for introduction patterns.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.
This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.
A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In a component-based source code organization of Coq `intf` doesn't
fit very well, as it sits in bit of "limbo" between different
components, and indeed, encourages developers to place types in
sometimes random places wrt the hierarchy. For example, lower parts of
the system reference `Vernacexpr`, which morally lives in a pretty
higher part of the system.
We move all the files in `intf` to the lowest place their dependencies
can accommodate:
- `Misctypes`: is used by Declaremod, thus it has to go in `library`
or below. Ideally, this file would disappear.
- `Evar_kinds`: it is used by files in `engine`, so that seems its
proper placement.
- `Decl_kinds`: used in `library`, seems like the right place. [could
also be merged.
- `Glob_term`: belongs to pretyping, where it is placed.
- `Locus`: ditto.
- `Pattern`: ditto.
- `Genredexpr`: depended by a few modules in `pretyping`, seems like
the righ place.
- `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and
could be fixed, as this module should be declared in `interp` which
is the one eliminating it.
- `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed
as it contains stuff it shouldn't. The right place should be `parsing`.
- `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`.
- `Notation_term`: First place used is `interp`, seems like the right place.
Additionally, for some files it could be worth to merge files of the
form `Foo` with `Foo_ops` in the medium term, as to create proper ADT
modules as done in the kernel with `Name`, etc...
|
| |\ \ |
|
| |\ \ \ |
|
| | |_|/
|/| |
| | | |
This changed in https://github.com/coq/coq/commit/35961a4ff5a5b8c9b9786cbab0abd279263eb655
|
| | |/
|/| |
|
| | |
| |
| |
| |
| |
| | |
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
|
Emilio Jesus Gallego Arias
Rin Arakaki
Pierre-Marie Pédrot
Siddharth Bhat
Théo Zimmermann
Hugo Herbelin
Maxime Dénès
Gaëtan Gilbert
Jim Fehrle
Paul Steckler
Matthieu Sozeau
Jasper Hugunin