| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
PR #13183 introduced quite a bit of duplicate code, we refactor it and
expose less internals on the way. That should make the API more
robust.
|
|
|
|
Towards #5154 (but insufficient)
|
|
|
|
Reviewed-by: ppedrot
|
|
function
Reviewed-by: ejgallego
|
|
|
|
Deprecated since #12034 (8.12)
|
|
This patch is trying to upstream a jsCoq patch that was written to
solve Stack Overflow issues:
https://github.com/jscoq/jscoq/blob/v8.12/etc/patches/cps.patch
It turns List.fold_right in vernac/declaremods into List.fold_left
on a reversed lit.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
section/module closing time
Reviewed-by: SkySkimmer
|
|
|
|
Fixes #13755 .
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
|
|
|
|
inductive definitions.
Reviewed-by: SkySkimmer
|
|
We deprecate unspecified locality as was done for Hint.
Close #13724
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
|
|
This returns to the previous behaviour of Implicit Type forgetting
universes.
`Implicit Type T : Type@{u}.` may be confusing as it is equivalent to
`: Type`, but until we have a better idea of what to do with anonymous
types I see no other solution, especially in the short term to fix the
bug.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
|
|
Reviewed-by: SkySkimmer
|
|
We expose the representation function in UGraph and change the printer
signature to work over the representation instead of the abstract type.
Similarly, the topological sorting algorithm is moved to Vernacentries.
It is now even simpler.
|
|
|
|
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
|
|
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
|
|
Namely, WrongNumargInductive and WrongNumargConstructor.
|
|
We also simplify the whole process of interpretation of cases pattern
on the way.
|
|
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
This avoids doing it repeatedly for nothing in intern/extern.
|
|
They are not used there, and removing the redundance of the the case
representation requires access to the environment, so we push their use
further up.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: herbelin
Ack-by: jfehrle
|
|
Reviewed-by: Zimmi48
|
|
|
|
As discussed in the Coq meeting.
|
|
|
|
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: mattam82
|
|
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.
|
|
|
|
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...
|
