| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
This allows proper treatment in notations, ie fixes #13303
The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).
This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:
~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~
When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.
Extern has a symmetrical problem:
~~~coq
Module Import M. Universe i. End M.
Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
Print foo. (* must not print Type@{i} -> Type@{i} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)
Therefore extern also takes a universe binders argument.
Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)
As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.
Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.
|
|
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
|
|
The bot merge was changed some time ago.
|
|
|
|
fix #11170).
Reviewed-by: gares
Reviewed-by: xavierleroy
Ack-by: ppedrot
|
|
Reviewed-by: erikmd
Reviewed-by: silene
Ack-by: mattam82
Ack-by: Blaisorblade
Ack-by: gares
Ack-by: Zimmi48
Ack-by: SkySkimmer
Ack-by: ejgallego
|
|
Reviewed-by: ppedrot
|
|
A few libraries in the CI don't compile with it
(out of memory).
|
|
Accumulators can grow arbitrarily large, even when well-typed. So, this
commit makes sure they are allocated on the major heap when they are too
large. If so, fields need to be filled with caml_initialize, in case they
point to the minor heap.
|
|
|
|
|
|
The old code was a mess of handwritten ad-hoc code to print the result table
in a fancy way. Instead of hardcoding everything this patch introduces a
generic function to print a table of data. This will allow extension of the
profiling information displayed to the user in an easy way.
|
|
Reviewed-by: Zimmi48
Reviewed-by: SkySkimmer
Ack-by: gares
|
|
Reviewed-by: MSoegtropIMC
|
|
|
|
Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: ppedrot
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
|
|
- closes #12376 : dune version is now consistent as suggested
- cc #12858 : coqide and coqide-server do no depend on ocamlfind
when built this way.
- closes #13372 : more precision in the license identifier
|
|
This was broken since #13177. We remove support for user overlays in
Windows build instead of fixing it since there is no specific use
case.
|
|
We re-expose `declare_projections` and `declare_structure_entry` as it
is needed by coq-elpi.
Ideally we would provide a better way in recordops to interact with
this, in fact `declare_structure_entry` is just a wrapper around
recordops + libobject structure so there is hope it goes away entirely
in the future.
The need for Elpi to manually call `declare_projections` should
actually disappear in future refactorings.
|
|
Reviewed-by: gares
Ack-by: SkySkimmer
Ack-by: ejgallego
|
|
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Reviewed-by: ejgallego
Ack-by: RalfJung
Ack-by: Zimmi48
|
|
|
|
Also add nice error message when the grep produces an empty result
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48
|
|
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: ejgallego
|
|
Git wants an identity and none is setup on the CI.
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
IMO it makes more sense this way, also it's more convenient if someone
wants to run the script locally.
|
|
|
|
Note: "hyp" was documented in Ltac Notation chapter but "var" was not.
|
|
time and use location in some typing error messages
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: MSoegtropIMC
|
|
Reviewed-by: mattam82
Ack-by: Janno
Ack-by: gares
|
|
This avoids the need to rebase the overlay when nothing has changed.
|
