| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
variables
|
|
One didn't normalize the bodies of fixpoints according to the universe
context, resulting in a type errors. Use EConstr.to_constr to ensure
universes are normalized instead of using EConstr.Unsafe.to_constr.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
then only parsing
|
|
|
|
Notations were not initially designed to support independent parsing
and printing rules. Some redesign of this part of the code shall be
necessary at some time.
|
|
Earlier, the nat_syntax_plugin was loaded as soon as Datatypes.v.
This would now implies to make Datatypes.v depends on Decimal.v.
Instead, we postpone the Numeral Notation for nat until Prelude.v,
and we adapt those three tests that happen to live strictly between
Datatypes and Prelude.
|
|
(NB: only variables whose binder is inside the constructor argument,
ie
Inductive foo := C : forall A : Type -> Type, A Type -> foo.
does not trigger the bug because A becomes a RelKey.)
|
|
This change is based on noticing that we use a default value for the
`sideff` argument even though we have a similarly named `side_eff`
available. Someone who knows how side effects and universes are
supposed to interact should check this.
|
|
|
|
Même causes, mêmes effets, similar fix to #8119:
- Do not pass let-bound arguments to evars.
We seize the opportunity to remove the useless type information for Aevar.
Special fixes to native compilation:
- Evars are not handled correctly when iterating over lambda terms.
- Names.id_of_string is gone.
- Evar instances are not reified in the right order.
|
|
|
|
which has no matching clauses.
|
|
Internal lemmas are inlined in obligations bodies, hence their universes
have to be declared with the obligations themselves. ~sideff:true was
not including the side effects universes and constraints in that case.
|
|
|
|
If a term is matched only against variables, it will not introduce a
"match" and thus, even if the term is of an inductive type, its
indices will not be taken into account in the current algorithm
(though one could imagine an algorithm which does an expansion
specially in order to filter on indices).
This allows to tell the unification not to use dependencies which the
pattern-matching algorithm is not able to exploit in practice.
See example in file 2733.v.
|
|
There were actually two broken things with VM + evars, the fixes are:
- Do not pass let-bound arguments to evars.
- Use the right order for evar arguments.
Native compilation seems to be suffering from the same shortcomings, I will
open a separate bug and adapt the PR.
|
|
No reason not to collapse inner applications with explicit arguments.
This is compatible with the ad hoc encoding of @f as GApp(f,[])/NApp(f,[]).
|
|
|
|
|
|
Closes #7967.
|
|
We use a more abstract representation for accumulators in the native
compilation scheme, that requires less fiddling with low-level implementation
details. It might be slower though.
|
|
|
|
|
|
|
|
|
|
|
|
We fix the issue by removing terms of the substitutions which have
free variables and are thus not interpretable in the context of the
"ltac:" subterm.
This remains rather ad hoc, since, in an expression "Notation f x :=
ltac:(foo)", we interpret "x" at calling time of "foo" rather than at
use time of "x" in foo, even if "x" is not necessary.
We could also imagine that binders in the ltac expressions are then
interpreted but that would start to be (very) complicated.
Note that this will presumably "fix" ltac2 quotations at the same
time.
|
|
subtyping.
|
|
|
|
When inferring [u <= v+k] I replaced the exception and instead add
[u <= v]. This is trivially sound and it doesn't seem possible to have
the one without the other (except specially for [Set <= v+k] which was
already handled).
I don't know an example where this used to fail and now succeeds (the
point was to remove an anomaly, but the example
~~~
Module Type SG. Definition DG := Type. End SG.
Module MG : SG. Definition DG := Type : Type. Fail End MG.
~~~
now fails with universe inconsistency.
Fix #7695 (soundness bug!).
|
|
It seems that lifting a term with a negative index is not equivalent to
strengthening it by applying to a dummy substitution. This looks suspicious
at best.
|
|
The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
|
|
|
|
|
|
Although the fix is not a proper one, it seems to solve
every instance of #2800 that could be tested.
|
|
to anomaly)
|
|
in unification
|
|
This is a quick fix. Code should be made nicer along these lines:
- try to pass the name of the variable created by "mkletin_goal" in
the monad using "refine_one";
- use a disjunctive type of "inhyps" to indicate when it is
meaningful, rather than using [].
|
|
|
|
Redundancy between finding section variables in both interp_var and
interp_qualid could probably be cleaned.
|
|
Fix #5012.
|
|
We store the universe context in the inlined terms and apply it to
the instance provided to the substitution function. Technically the
context is not needed, but we use it to assert that the length of the
instance corresponds, just in case.
|
