| Age | Commit message (Collapse) | Author |
|---|
|
|
|
The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of
integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been
replaced with `cl_typ` and `ClTypMap` respectively.
|
|
|
|
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.
|
|
Also some dead code.
If no typo is introduced, there should be no semantic changes.
|
|
An h-box inhibits the breaking semantics of any cut/spc/brk in the
enclosed box.
We tentatively replace its occurrence by an h or hv, assuming in
particular that if the indentation is not 0, an hv box was intended.
|
|
See https://github.com/coq/coq/pull/12875#issuecomment-679190489.
|
|
That is, in "About", use _ for the variables of the extra lists.
See discussion at https://github.com/coq/coq/pull/12875#issuecomment-679190489.
|
|
validated.
|
|
|
|
|
|
This is an alternative to #12663 ; much preferable as the kind
information is already stored in the constant object.
|
|
Now that `Printmods` is above `Declaremods`, we don't need to pass the
extra `mod_ops` argument.
|
|
This should make the univbinders output test less fragile as it
depends less on the global counter (still used for universes from
section variables).
|
|
This seems to be a pattern used quite a bit in the wild, it does not hurt
to be a bit more lenient to tolerate this kind of use. Interestingly the
API was already offering a similar generalization in some unrelated places.
We also backtrack on the change in Floats.FloatLemmas since it is an instance
of this phenomenon.
|
|
Ack-by: herbelin
|
|
Add headers to a few files which were missing them.
|
|
|
|
information may impact the display of coercion and implicit arguments.
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
|
|
|
|
Reviewed-by: maximedenes
|
|
|
|
The `Print Canonical Projections` command now can take constants and prints only
the unification rules that involves or are synthesized from given constants.
|
|
We restrict to those that are actually related to typeclasses, and
perform the following renamings:
Classops --> Coercionops
Class --> ComCoercion
|
|
The patch is done in a minimal way. The hacks are turned into a new kind of
safer hacks, but hacks nonetheless. They should go away at some point, but
the current patch is focussed on the removal of Libobject cruft, not making
the dirty code of its upper-layer callers any cleaner.
|
|
This governs the printing of the explicitation of implicit arguments
and the removal of coercions.
E.g., "Check coe foo." where coe is a coercion with codomain B will show:
foo
: B
instead of
coe foo
: B
|
|
This moves the encoding of "n" as "arg_n" closer to the user interface level.
Note however that Constrintern.build_impl is not able yet to use ExplByPos.
See further commits.
|
|
ie keep the fake arguments "/" and "&" instead of getting their index
at parsing time.
|
|
`Prettyp` is now late enough in linking to refer to them.
|
|
|
|
Close #10961
|
|
|
