| Age | Commit message (Collapse) | Author |
|---|
|
Conversely, Type existential variables now (explicitly) cover the Set
case.
Similarly for Prop and SProp.
|
|
We consistently use:
- UUnknown: to mean a rigid anonymous universe
(written Type in instances and Type as a sort)
[was formerly encoded as [] in Type's argument]
- UAnonymous: to mean a flexible anonymous universe
(written _ in instances and Type@{_} as a sort)
[was formerly encoded as [None] in Type's argument]
- UNamed: to mean a named universe or universe expression
(written id or qualid in instances and Type@{id} or Type@{qualid} or more
generally Type@{id+n}, Type@{qualid+n}, Type@{max(...)} as a sort)
There is a little change of syntax: "_" in a "max" list of universes
(e.g. "Type@{max(_,id+1)}" is not anymore allowed. But it was
trivially satisfiable by unifying the flexible universe with a
neighbor of the list and the syntax is anyway not documented.
There is a little change of semantics: if I do id@{Type} for an
abbreviation "id := Type", it will consider a rigid variable rather
than a flexible variable as before.
|
|
This feature makes it possible to tell type inference to type
applications of a global `foo` using typing information from the context
once the `n` first arguments are known.
The syntax is: `Arguments foo x y | z`.
Closes #7910
|
|
|
|
|
|
|
|
|
|
Ack-by: ejgallego
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
prevent them from being “canonical”
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: robbertkrebbers
Ack-by: vbgl
|
|
Reviewed-by: SkySkimmer
|
|
I don't think there's a reason to treat such variables more severely
than unbound variables. This anomaly is often raised by debug printers
(e.g. when studying complex scenarios using `Set Unification Debug`),
and so makes debugging less convenient.
Fixes #3754, fixes #10026.
|
|
|
|
|
|
Incidentally, this fixes #10056
|
|
Some of them are significant so presumably it will take a bit of
effort to fix overlays.
I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
|
|
whd_betaiota_deltazeta_for_iota_state.
Reviewed-by: herbelin
|
|
There is no point, it is always called with refolding turned off.
|
|
|
|
This was introduced by @herbelin in
817308ab59daa40bef09838cfc3d810863de0e46, appears to have been
made unnecessary again by herbelin in
4dab4fc5b2c20e9b7db88aec25a920b56ac83cb6.
At this point it appears to be completely unused.
|
|
|
|
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: herbelin
Reviewed-by: mattam82
Ack-by: maximedenes
|
|
Fixes #6699
|
|
We make clearer which arguments are optional and which are mandatory.
Some of these representations are tricky because of small differences
between Program and Function, which share the same infrastructure.
As a side-effect of this cleanup, Program Fixpoint can now be used with
e.g. {measure (m + n) R}. Previously, parentheses were required around
R.
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
I had to reorganize the code a bit. The Context command moved to
comAssumption, as it is not so related to type classes. We were able to
remove a few hooks on the way.
|
|
|
|
One other call still remains, but will require to refactor some
section-handling code.
|
|
|
|
As per the OCaml documentation, the order for maps should be total.
I also remove some circumvolutions that were added around eliminators
and canonical names because of this incorrect order.
|
|
We already have indirection (constant -> effect name, effect name ->
function) so we only need to stop using summary.ref for the second map.
|
|
Reviewed-by: gares
|
|
This was making an assertion fail on
https://github.com/coq/coq/issues/9684 after 23f84f37
|
|
This cache makes the pretyper depend on components that should morally
be higher-level (Libobject and co), so I'd like to see how critical this
cache is before taking any action.
|
|
Ack-by: jfehrle
Ack-by: ppedrot
Reviewed-by: vbgl
|
|
Ack-by: JasonGross
Reviewed-by: ppedrot
|
|
We provide a flag that allows for a dumber but O(log n) algorithm generating
fresh names in detyping.
|
|
For now it does not change anything, but it will make the move towards a
faster algorithm seamless.
|
|
There was a hidden bug to an unexpected variable capture in decomp_branch.
Let us use proper structures to avoid this kind of mess.
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
(warn if bar is a nonprimitive projection)
|
