| Age | Commit message (Collapse) | Author |
|---|
|
As discussed in the Coq meeting.
|
|
Co-authored-by: <Théo Zimmermann <theo.zimmermann@inria.fr>
|
|
|
|
Most cases should be accounted in proof code, however be wary of paths
where `Global.env ()` is used.
|
|
The syntax is the one of boolean attributes, that is to say
`#[typing($flag={yes,no}]` where `$flag` is one of `guarded`,
`universes`, `positive`.
We had to instrument the pretyper in a few places, it is interesting
that it is doing so many checks.
|
|
|
|
This is just an experiment, but makes the uses of the API easier as we
don't mess with the global state anymore.
|
|
We use the new `Declare.Info` structure to uniformly add properties to
the handling of constants. In this case, per-constant typing flags.
The internal code may want to see some further refactoring, including
pushing the flags down to `Safe_typing.add_constant` , but the changes
in the interface should be definitive.
This will allow #12539 and #9004 using attributes.
|
|
Reviewed-by: SkySkimmer
Ack-by: silene
|
|
|
|
|
|
|
|
In this way interval does not have to wait too much
|
|
Reviewed-by: mattam82
|
|
Reviewed-by: SkySkimmer
|
|
gtk im modules
Reviewed-by: gares
|
|
|
|
|
|
|
|
evars
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
Reviewed-by: herbelin
|
|
|
|
This was changed from so to dylib in dd7c679cf6, but it seems to
depend on versions of gtk. Accepting both seems ok, assuming that at
least one will work.
|
|
|
|
|
|
|
|
Reviewed-by: ppedrot
Ack-by: vbgl
|
|
|
|
|
|
|
|
- rename @{u} to @{uu} (u is the default name so using @{u} doesn't
test as much as it should)
- move part of the test using Require to end of the file (when quickly
testing changes this allows to run most of the test without compiling
the Require'd file)
|
|
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: gares
|
|
Reviewed-by: vbgl
|
|
Reviewed-by: Zimmi48
Ack-by: JasonGross
|
|
|
|
|
|
|
|
|
|
|
|
Instead of loading the whole file in memory, we simply load an index table
associating a file position to a key hash. Cache access is then performed
on the fly by unmarshalling the data whose hash corresponds and checking
key equality.
|
|
For some reason it was explicitly deactivated since the file was added, but
I have no idea why. Unsetting sharing would lead to potential explosive
memory consumption at unmarshalling time which is not worth the minimal cost
it has at marshalling time.
|
|
|
|
coercion not being used
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
To tie the knot (since the evar depends on the evar type and the
source of the evar type of the evar), we use an "update_source"
function.
An alternative could be to provide a function to build both an evar
with its evar type directly in evd.ml...
|
