| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
Because refreshing Prop is not semantics-preserving,
the new universe is >= Set, so cannot be minimized to Prop
afterwards.
|
| |
|
|
|
|
|
| |
In congruence, refresh universes including the Set/Prop ones so that
congruence works with cumulativity, not restricting itself to the
inferred types of terms that are manipulated but allowing them to be
used at more general types. This fixes bug #4609.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
But there are still bugs with Declare Implicit Tactic, which should
probably rather be reimplemented with ltac:(tac).
Indeed, it does support evars in the type of the term, and
solve_by_implicit_tactic should transfer universe constraints to the
main goal. E.g., the following still fails, at Qed time.
Definition Foo {T}{a : T} : T := a.
Declare Implicit Tactic eassumption.
Goal forall A (x : A), A.
intros.
apply Foo.
Qed.
|
| |
|
|
| |
They can apply to the head reference under a notation.
|
| |
|
|
|
|
| |
internalization.
Patch by PMP, test-suite fix by MS.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When typing a "with clause fails, type classes are used to possibly
help to insert coercions. If this heuristic fails, do not consider it
anymore to be the best failure since it has made type classes choices
which may be inconsistent with other constraints and on which no
backtracking is possible anymore (see new example in test suite file
4782.v).
This does not mean that using type classes at this point is good. It
may find an instance which help to find a coercion, but which might
still be a choice of instance and coercion which is incompatible with
other constraints.
I tend to think that a convenient way to go to deal with the absence
of backtracking in inserting coercions would be to have special
For the record, here is a some comments of what happens regarding
f9695eb4b and 827663982.
In the presence of an instance (x:=t) given in a "with" clause, with
t:T, and x expected of type T', the situation is the following:
Before f9695eb4b:
- If T and T' are closed and T <= T' is not satisfiable (no coercion
or not convertible), the test for possible insertion of a coercion
is postponed to w_merge, even though there is no way to get more
information since T ant T' are closed. As a result, t may be
ill-typed and the unification may try to unify ill-formed terms,
leading to #4872.
- If T and T' are not closed and contains evars of type a type class,
inference of type classes is tried. If it fails, e.g. because a
wrong type class instance is found, it was postponed to w_merge as
above, and the test for coercion is retried now interleaved with
type classes.
After f9695eb4b and 827663982e:
- If T and T' are closed and T <= T' is not satisfiable (no coercion
or not convertible), the test for possible insertion of a coercion
is an immediate failure. This fixes #4872.
- However, If T and T' are not closed and contains evars of type a
type class, inference of type classes is tried. If it gives closed
terms and fails, this is immediate failure without backtracking on
type classes, resulting in the problem added here to file 4872.v.
The current fix does not consider the result of the use of type
classes while trying to insert a coercion to be the last word on
it. So, it fails with an error which is not the error for conversion
of closed terms (ConversionFailed), therefore in a way expected by
f9695eb4b and 827663982e, and the "with" typing problem is then
postponed again.
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
Check that the polymorphic status of everything that
is parameterized in nested sections is coherent.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
The tentative fix in f9695eb4b (which I was afraid it might be too
strong, since it was implying failing more often) indeed broke other
things (see #4813).
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Trying to now catch all unification errors, but without a clear view
at whether some errors could be tolerated at the point of checking the
type of the binding.
|
| | | |
| | |
| | |
| | |
| | | |
Typically, a problem of the form "?x args = match ?y with ... end" was
a failure even if miller-unification was applicable.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The exact and e_exact tactics were not registering the universes and
constraints of the hint correctly. Now using the same connect_hint_clenv
as unify_resolve, they do. Also correct the implementation of
prepare_hint to normalize the universes of the hint before abstracting
its undefined universes. They are going to be refreshed at each
application. This means that eauto using term can
use multiple different instantiations of the universes of term
if term introduces new universes. If we want just one instantiation
then the term should be abbreviated in the goal first.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Some dubious evarmap manipulation is going on in destruct because of the
use of clenv primitives. Here, building a clenv was introducing new evars
that were not taken into account in the remainder of the tactic. We plug
them back using a local workaround.
Eventually, this code should be replaced by an evar-based one, but meanwhile,
we rely on what is probably a hack.
|
| | | |
|
| |/
|
|
|
|
|
| |
- In Program, a check_evars_are_solved was introduced
too early. Program does it's checking of evars by itself.
- In Function, the universe environments were not threaded
correctly.
|
| |
|
|
|
| |
Use the compatibility match construction to extract the compatibility
constant associated to a primitive projection.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Fix handling of non-polymorphic hints built from polymorphic values, or
simply producing new universes. We have to record the side effects of
global hints built from constrs which are not polymorphic when they
declare global universes, which might need to be discharged at the end
of sections too. Also issue a warning when a Hint is declared for a
polymorphic reference but the Hint isn't polymorphic itself (this used
to produce an anomaly). For [using] hints, treat all lemmas as
polymorphic, refreshing their universes at each use, as is done for
their existentials (also used to produce an anomaly).
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
Note that extracting terms containing primitive projections is still
utterly broken, so don't use them.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
preserved, which is a source of incompatibilities w.r.t. released 8.5
but which looks to me to be the only possible canonical behavior.
This is I believe a better behavior than the Regular Subst Tactic
behavior in the released 8.5 and 8.5pl1. There, the order of
hypotheses in which substitutions happened was respected, but their
interleaving with other hypotheses was not respected.
So, I consider this to be a fix to the "Regular Subst Tactic" mode.
Also added a more detailed "specification" of the "Regular" behavior
of "subst" in the reference manual.
|
| |
|
|
| |
rejected.
|
| | |
|
| | |
|
| |
|
|
| |
Disclaimer: I have no idea what I am doing.
|
| |
|
|
| |
Also register properly the kind of definition.
|
| | |
|
| |
|
|
|
|
|
|
| |
When a notation was starting or ending a space, Coq assumed the notation
had no terminal symbol in either places. Coq also considered a notation
containing only spaces to be productive. As stated in the documentation,
extraneous spaces are only meant as printing hints, they are not meant to
have any influence on parsing.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
When encountering a "simpl nomatch" constant, the reduction machinery tries
to unfold it. If the subsequent partial reduction does not produce any
match construct, it keeps going from the reduced term. Unfortunately, the
reduced term has been refolded in the meantime, which means that some of
the previous reduction steps have been canceled, thus causing an infinite
loop. This patch delays the refolding till the very end, so that reduction
always progresses.
Disclaimer: I have no idea what I am doing here. The patch compiles the
standard library and the test suite properly, so hopefully they contain
enough tests to exercise the reduction machinery.
|
| |
|
|
|
|
|
|
|
|
|
| |
As noticed by Cyprien Mangin, projected terms cannot directly be used as
head values. Indeed, they might be applications (e.g. constructors as in
the bug report) whose arguments would thus be missing from the evaluation
stack when doing any iota-reduction step.
The only case where it would make sense is when the evaluation stack is
empty, as an optimization. Indeed, in that case, the arguments are put on
the stack, and then immediately put back inside the term.
|
| |
|
|
|
| |
constants up to their canonical name (taken from Daniel's
formalization of Puiseux theorem).
|
| | |
|
| |
|
|
|
| |
while eta-expanding a notation) + a more serious variant of it
(alpha-conversion incorrect wrt eta-expansion).
|
| |
|
|
|
|
|
|
|
|
|
| |
This is a follow-up on Matthieu's 7e7b5684
The Definition command was classified incorrectly when a body was provided.
This fix is a bit ad-hoc. A better one would require more expressiveness in
side effect classification, but I'll do it in trunk only since it could impact
plugins.
Thanks a lot to Enrico for his help!
|
| |
|
|
|
|
| |
Falling back to the global setting if not given.
Useful to make Add Morphism fail correctly when the given proof terms
are incomplete. Adapt test-suite file #2848 accordingly.
|
| |
|
|
|
| |
Passing `-compat 8.4` now allows the use of `econstructor (tac)`, as in
8.4.
|
| |
|
|
|
| |
I introduced this bug in 4c078b0362542908eb2fe1d63f0d867b339953fd;
Coq.Init.Notations.constructor does not take any arguments.
|
| |
|
|
|
| |
As if we were adding : Type. Consistent with inductives with no
declared arity.
|
| | |
|
| | |
|
| |
|
|
| |
Forcefully equating it to the inferred level is not always desirable or possible.
|
| |
|
|
| |
So adding a test-suite file and closing the bug.
|
| |
|
|
|
|
|
|
|
| |
E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive
records with eta for which conversion is incomplete.
- Eta-conversion only applies to BiFinite inductives
- Finiteness information is now checked by the kernel (the constructor types
must be strictly non recursive for BiFinite declarations).
|
| |
|
|
| |
They were not parsed correctly with a newline in the middle.
|
| |
|
|
| |
Add test-suite file to ensure non-regression.
|
Matthieu Sozeau
Maxime Dénès
Hugo Herbelin
Matthieu Sozeau
Pierre-Marie Pédrot
Guillaume Melquiond
Jason Gross