| Age | Commit message (Collapse) | Author |
|---|
|
3cd718c, to the case of second_order_matching.
|
|
|
|
not using the intended test. By fixing the intended test, the need for
a delta-expansion resulting from this commit in PFsection6.v (line
1255) of ssreflect disappears.
|
|
unification algorithm in consider_remaining_unif_problems. If it
happens to be problematic, one can backtrack to the "optimization"
from 3bd9cb26b which has a restriction on rels/vars.
|
|
|
|
following working:
Definition test {A B:Type} {H:A=B} (a:A) : B := rew H in a.
|
|
initial segment of the context of the evar.
|
|
environment.
A closure is supposedly closed: all the relevant Ltac variables should be then. The last field [ltac_genargs], if I'm not mistaken, is there to represent the Ltac variables which are bound but not to something which makes sense in a term. They should be irrelevant at this point, since the uconstr has already been interpreted and these checks are supposed to have happened. (though I'm not entirely sure they do, it can be an interesting exercise to try and make [uconstr] behave weirdly)
I'm not quite sure why it caused #3679, though. But it still seems to be solved.
|
|
accidentally mixed up in 9aa416c0c6.
|
|
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
|
|
Patch by CJ on bugzilla. CUnix.sys_command doesn't rely on a shell, so extra
care with cmd.exe vs sh is no longer required.
|
|
step, prefer QuestionMark's to other evars, to comply with the
filtering made on VarInstance, GoalEvar and QuestionMark for type
class resolution. Maybe evars to be resolved by type class instances
should eventually be marked with a specific tag.
At least, this solves the current problem with compiling cancel2.v in
LemmaOverloading.
|
|
unification flags (see also temporary revert in d083200ae5b).
|
|
|
|
|
|
You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
|
|
- In evarconv, check_conv_record properly computes the parameters of
primitive record projections for later unification, adding env and
sigma as arguments.
- In unification, backtrack on pattern-unification and not only
application unification if eta for a record failed.
|
|
Revert "Fixing an evar_map bug revealed by commit 603b66f81 on unification flags."
This reverts commit d083200ae5b391ceffaa0329a8e3a334036c7968.
|
|
in reporting the chain of causes when unification fails.
|
|
|
|
pattern-matching predicate.
|
|
This fixes current failure of RelationAlgebra.
|
|
In the case of conversion, postponing by preserving the
initial orientation.
Was wrong from its initial version in Jan 2014, but was not visible
because evar-evar subtyping was approximated by evar-evar conversion.
Thanks to Enrico for a very short example highlighting the problem. In
particular, this fixes Ergo.
|
|
test pattern-unification after restriction of the evars so as to
succeed earlier (no observational changes however in the examples at my
disposal).
|
|
e.g. for MTac.
|
|
|
|
|
|
?n[...] = ?p[...;x:=?n[...];...]. Indeed, x could be a solution for ?p.
|
|
similar optimization broke at some time some ssreflect code; we now
treat the easy case of a let-in to a rel - a pattern common in
pattern-matching compilation -; later on, we shall want to investigate
whether any let-in found to refer to out of scope rels or vars can be
filtered out).
|
|
|
|
|
|
|
|
|
|
- new function set_flags_for_type for setting flags when converting
types of the terms to unify
- it now sets all conversion flags, possibly restricting delta using
modulo_delta_types
- it is now used in w_unify_core_0 too
- fixing/improving documentation of options
- deprecating "Set Tactic Evars Pattern Unification"
|
|
types: we downcast the evar in the higher type to the lower type.
Then, we have the freedom to choose the order of instantiation
according to the instances of the evars (e.g. choosing the
instantiation for which pattern-unification is possible, if ever it is
possible in only one way - as shown by an example in contribution
Paco).
This still does not preserve compatibility because it happens that
type classes resolution is crucially dependent on the order of
presentation of the ?n=?p problems. Consider e.g. an example taken
from Containers. Both now and before e2fa65fccb9, one has this asymmetry:
Context `{Helt : OrderedType elt}.
Check forall x y r l h, @Equivalence.equiv _ _ _ x y -> In x (Node l x r h).
--> @Equivalence.equiv QArith_base.Q QArith_base.Qeq QArith_base.Q_Setoid x y
Context `{Helt : OrderedType elt}.
Check forall x y r l h, In x (Node l x r h) -> @Equivalence.equiv _ _ _ x y.
--> @Equivalence.equiv elt (@_eq elt Helt) (@OT_Equivalence elt Helt)
Then, embedding this example within a bigger one which relies on the
?n=?n' resolution order, one can get two incompatible resolution of
the same problem.
To be continued...
|
|
The occur check is done even if the flag [unsafe] is set to true. The rational is that a tactic cannot control where it takes pieces of terms from (and hence will not generally make terms which pass the occur-check), and it would be painful to ask every tactic which takes a term as an argument to do an occur check before [refine].
I reused the same error than used by unification. It gives a pretty nice error message. An alternative would be to have a dedicated error with pretty much the same error message. I'm not sure which is best, so I went for the simplest one.
The same check is done in the compatibility layer.
Fixes a reported bug which I cannot locate for some reason.
|
|
full instances.
|
|
types as it was before commit 710bae2a8c81a44.
There is still at least one problem with bug #3392 to solve.
|
|
possible, which is the "natural" way to orient an equation. At least
it matters for matching subterms against patterns, so that it is the
pattern variables which are substituted if ever the subterm has itself
existential variables, as in:
Goal exists x, S x = x.
eexists.
destruct (S _).
|
|
arbitrary direction as if it were an "evar = evar" problem.
|
|
Incidentally, this allows to make earlier the collapse of CUMUL to
CONV when force is true.
|
|
evar_define.
Interestingly, the added choose in evarconv.ml allows solve_evar_evar
to be observationally commutative, in the sense of not either fail or
succeed in compiling the stdlib whether problems are given in the
left-to-right or right-to-left order.
|
|
subsumed by the call to project_evar_on_evar.
|
|
- Registering strict implicit arguments systematically (35fc7d728168)
- Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6)
- Fixing Coq compilation (894a3d16471)
Systematically computing strict implicit arguments can lead to big
computations, so I suspend this attempt, waiting for improved
computation of implicit arguments, or alternative heuristics going
toward having more conversion in rewrite.
|
|
|
|
in tactic unification.
|
|
|
|
while before these were supposed to consider only syntactically.
Made the experiment to unify with all delta flags unset. Keeping the
same flags as for non evar/meta free subterms would lead to too much
successes, as e.g. "true && b" matching "b" when the
modulo_conv_on_closed_terms flag is set, which is the case for
rewrite. But maybe should we instead investigate to have the same
flags but with the restrict_conv_on_strict_subterms flag set. This
rules out examples like "true && b" unifying with "b" and this is
another option which is ok for compiling the stdlib without any
changes.
|
|
This bug was affecting the VM and the native compiler, but only in the pretyper
(not the kernel). Types of arguments of fixpoints were incorrectly normalized
due to a missing lift.
|
|
|
