| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: herbelin
Ack-by: jfehrle
|
|
Reviewed-by: gares
|
|
check resolution of evars more incrementally
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
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.
|
|
incrementally.
The regression was due to #12365. We fix it by postponing the evars
check after the calls to the underlying constructor tactic, while
retaining using information from the first instantiations to resolve
the latter instantiations.
|
|
Reviewed-by: mattam82
|
|
evars
Reviewed-by: SkySkimmer
|
|
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
|
|
|
|
coercion not being used
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...
|
|
of universes in "Context"
Reviewed-by: SkySkimmer
|
|
|
|
Fixes #13453 which was a loop in
~~~ocaml
let normalize a =
let o = optims () in
let rec norm a =
let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in
if eq_ml_ast a a' then a else norm a'
in norm a
~~~
the `eq_ml_ast` was always returning `false`.
|
|
|
|
|
|
same time (granting #9816)
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
fix #11170).
Reviewed-by: gares
Reviewed-by: xavierleroy
Ack-by: ppedrot
|
|
In #11172, an "=" on the number of arguments of an applied coercion
had become a ">" on the number of arguments of the coercion. It should
have been a ">=". The rest of changes in constrextern.ml is "cosmetic".
Note that in #11172, in the case of a coercion to funclass, the
definition of number of arguments of an applied coercion had moved
from including the extra arguments of the coercion to funclass to
exactly the nomber of arguments of the coercion (excluding the extra
arguments). This was necessary to take into account that several
coercions can be nested, at least of those involving a coercion to
funclass.
Incidentally, we create a dedicated output file for notations and
coercions.
|
|
|
|
Reviewed-by: ejgallego
|
|
in notations
Reviewed-by: ejgallego
Ack-by: Zimmi48
Ack-by: jfehrle
|
|
Reviewed-by: erikmd
Reviewed-by: silene
Ack-by: mattam82
Ack-by: Blaisorblade
Ack-by: gares
Ack-by: Zimmi48
Ack-by: SkySkimmer
Ack-by: ejgallego
|
|
|
|
|
|
|
|
|
|
between variable and non-qualified global references
Reviewed-by: ejgallego
Ack-by: maximedenes
Ack-by: gares
|
|
instead of recursive make
|
|
an arity.
Reviewed-by: ppedrot
|
|
|
|
binder
Reviewed-by: herbelin
|
|
primitive projection was wrongly supposed to be already inferred
Reviewed-by: gares
|
|
template poly
Reviewed-by: gares
Reviewed-by: herbelin
|
|
type.
This was a case where expand_projections was calling find_mrectype
which was expecting the argument of the projection to be an inductive.
We could have ensured that this type is at least the appropriate
inductive applied to fresh evars, but this expand_projections was in
practice used for checking the applicability of canonical structures
and the unifiability of the parameters of the projections is anyway a
consequence of the unifiability of the principal argument of the
projections. So, the latter is enough.
|
|
Ack-by: ppedrot
Reviewed-by: proux01
|
|
then by last imported
Reviewed-by: Zimmi48
Ack-by: RalfJung
Ack-by: gares
|
|
|
