| Age | Commit message (Collapse) | Author |
|---|
|
(and not just…
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
unification error message
Reviewed-by: ppedrot
|
|
The `Print Canonical Projections` command now can take constants and prints only
the unification rules that involves or are synthesized from given constants.
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
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.
|
|
|
|
|
|
clearer.
|
|
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.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
We restrict to those that are actually related to typeclasses, and
perform the following renamings:
Classops --> Coercionops
Class --> ComCoercion
|
|
This highlights the fact that diamond inheritance of a custom entry
is a tricky problem, as well as merely importing two custom entries with
the same name from two different modules. The only sane way to give a
semantics to that is to stick to module-scoped objects, i.e. give those
entries a kernel name. In the meantime, I went for a warning when
overriding entries.
|
|
Fixes #9532
Fixes #9490
|
|
~strict flag
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
It gets thrown away if the inductive is declared in a section anyway,
and there is no user syntax to specify it.
|
|
take only the template_check flag instead of the whole env
|
|
We do [solve_remaining_evars all_and_fail_flags] immediately before
calling [interp_mutual_inductive_constr] so these checks are extra.
|
|
There are no users in Coq but maybe some plugin wants it so don't
completely remove it
|
|
One should generally push contexts with ~strict:true when the context is a monomorphic one (all univs > Set) except for template polymorphic inductives (>= Prop) and ~strict:false for universe polymorphic ones (>= Set). Includes fixes from Gaëtan's and Emilio's reviews
|
|
if the .vos file is empty, rename -quick to -vio, dump empty .vos when producing .vio, dump empty .vos and .vok files when producing .vo from .vio.
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
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.
|
|
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.
|
|
Reviewed-by: JasonGross
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
And simplify a lot the compatibility infrastructure following this.
Update dev/tools/update-compat.py
Remove much complexity.
Co-authored-by: Jason Gross <jgross@mit.edu>
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: silene
|
|
Reviewed-by: SkySkimmer
Reviewed-by: cpitclaudel
|
|
Fixes #10573
|
|
|
|
Fixes #10576
|
|
|
|
and do not run template_candidate in the upper layers when the
template attribute is given.
This means we can use an over-approximation in the upper layer
implementation of template_candidate (returning false even in cases
which the kernel may accept) if we ever want to.
|
|
Using the parameter universes in the constructor causes implicit
equality constraints, so those universes may not be template
polymorphic.
A couple types in the stdlib were erroneously marked template, which
is now detected. Removing the marking doesn't actually change
behaviour though.
Also fixes #10504.
|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
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
```
|
|
cleaning
Reviewed-by: ejgallego
|
|
Reviewed-by: gares
Reviewed-by: silene
|
|
"similar" means sharing a scope or implicit status.
|
|
ie keep the fake arguments "/" and "&" instead of getting their index
at parsing time.
|
|
(fixing bug #11057).
With this new behavior, it is not needed to .vos files in user contribs.
Also, this commit adds a feature: upon creation of a .vo file, an empty .vok file is touched.
|
|
This is in accordance with PR #10614 and to avoid a confusion with the
fields of a record type in g_vernac.ml.
Removing a useless line at the same time in G_vernac.
|
