| Age | Commit message (Collapse) | Author |
|---|
|
Fix #13987
|
|
Namely, WrongNumargInductive and WrongNumargConstructor.
|
|
We also simplify the whole process of interpretation of cases pattern
on the way.
|
|
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...
|
|
|
|
|
|
This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.
|
|
This improves the error message on the example for #13171, however we
may question whether there should be an error at all.
|
|
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.
|
|
Reviewed-by: ejgallego
|
|
|
|
candidates.
We also show the incompatible contender.
Ideally, we should also remember the source of the other contender.
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
This should make the univbinders output test less fragile as it
depends less on the global counter (still used for universes from
section variables).
|
|
They were not used anywhere anymore.
|
|
This was useless, since we did not observe the difference on evars.
|
|
|
|
This corresponds more naturally to the use we make of them, as we don't need
fast indexation but we instead keep pushing terms on top of them.
|
|
Add headers to a few files which were missing them.
|
|
Raising inside exception printers is quite tricky as the order of
registration for printers will indeed depend on the linking order.
We thus forbid this, and make our API closer to the upstream
`Printexn` by having printers return an option type.
|
|
ie regardless of the Print Universes flag.
AFAICT there is no point in skipping them.
|
|
The previous system was from before globref was in the kernel.
|
|
Not sure if it's possible to see it without a plugin.
|
|
We don't need to handle `Dynlink` errors specially anymore.
|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional
environment instead of querying the imperative global one. We percolate
this change as higher up as possible.
|
|
Might be improvable further. In the first example, we have two
environments involved and one is implicit. It does not seem excluded
that a variable name of the second environment shows up which is not
listed in the first environment.
|
|
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
Now that we place imperative module declaration on top of module
interpretation we can remove the abstraction layer used in
`Declaremods`, so the `interp_modast` parameter goes away.
Improvement suggested by Gaëtan Gilbert.
|
|
We remove the special error printing pre-processing in favor of just
calling the standard printers.
Error printing has been a bit complex for a while due to an incomplete
migration to a new printing scheme based on registering exception
printers; this PR should alleviate that by completing the registration
approach.
After this cleanup, it should not be ever necessary for normal
functions to worry a lot about catching errors and re-raising them,
unless they have some very special needs.
This change also allows to consolidate the `explainErr` and `himsg`
modules into one, removing the need to export the error printing
functions. Ideally we would make the contents of `himsg` more
localized, but this can be done in a gradual way.
|
|
|
|
This replaces the mismatched context error, which occurred when
Instance := {} was used with strictly more fields than declared.
Since we later check that field names match those declared for the
instance, now that we reject duplicates we know that there are no
extra fields.
|
|
|
|
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.
|
|
|
|
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.
|
|
And document the error message.
|
|
This should make https://github.com/coq/coq/pull/9129 easier.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: jfehrle
|
|
|
|
For nonsquashed:
Either
- 0 constructors
- primitive record
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: vbgl
|
