| Age | Commit message (Collapse) | Author |
|---|
|
Pushing pending problems had the side-effect of later solving them in
the opposite order as they arrived, resulting on different complexity
(see e.g. #4076). We now take care of pushing them in reverse order so
that they are treated in the same order.
|
|
is_constrainable_in.
|
|
|
|
This was broken by the attempt to use the same algorithm for rewriting
closed subterms than for rewriting subterms with evars: the algorithm
to find subterms (w_unify_to_subterm) did not go through evars. But
what to do when looking say, for a pattern "S ?n" in a goal "S ?x[a:=S ?y]"?
Should we unify ?x[a:=S ?y] with ?n or consider ?x as rigid and look
in the instance? If we adopt the first approach, then, what to do when
looking for "S ?n" in a goal "?x[a:=S ?y]"? Failing? Looking in the
instance? Is it normal that an evar behaves as a rigid constant when
it cannot be unified with the pattern?
|
|
|
|
|
|
to display by default (see bc8a5357889 - 17 Oct 2014):
- not printing instances for let-in anymore even when expanded (since
they are canonical up to conversion)
- still printing x:=x in [x:=x;x':=x] when x is directly an instance
of another var, but not in [x:=x;x':=S x]
This can be discussed, but if ever this is to be changed, it should
not be printed in [x:=x;x:=?n] with ?n implicitly depending on x
(otherwise said, variables which are not displayed in instances of
internal evars should not contribute to the decision of writing
x:=x in the instance).
|
|
is_constrainable_in to do the job of ensuring that ?p does not belong to the ti while solving ?p[...]:=?n[t1..tn].
|
|
Bindings of the form [let x:T := M] are unfolded into [(M:T)], so that
occur-check is done in [T] as well as in [M] (except when [M] is a
variable, where it is hopefully not necessary).
This is a way to fix #4062 (evars with type depending on themselves).
The fix modifies the alias map (make_alias_map) but it should behave
the same at all places using alias maps other than
has_constrainable_free_vars.
|
|
|
|
goal in Instance. Also remove some dead code.
|
|
|
|
|
|
|
|
unifications ?X ~= ?Y foo not catched by solve_evar_evar.
|
|
from Matthieu).
|
|
|
|
|
|
|
|
Unifying two let-in's expresions syntactically is a heuristic
(compared to performing the zeta-reduction). This heuristic was
requiring unification of types which is too strong for the heuristic
to work uniformly since the types might only be related modulo
subtyping.
The patch is to remove the unification of types, which allows then to
have the heuristic work uniformly on the bodies. On the other side, I
hope it does not loose (still heuristical) unifications compared to
before (presumably, since instantiating the evars in the body will
induce constraints for solving potential evars in the types of the
let-in bodies, but this would need a proof). Anyway, it is not about
correction, it is about a heuristic, which maybe done too early
actually.
|
|
printing functions touched in the kernel).
|
|
match predicates for vm_compute and compile polymorphic definitions
to constant code. Add univscompute test-suite file testing VM
computations in presence of polymorphic universes.
|
|
One remaining issue: aliased constants raise an anomaly when some unsubstituted
universe variables remain. VM may suffer from the same problem.
|
|
definitions. Instead of failing with an anomaly when trying to do
conversion or computation with the vm's, consider polymorphic constants
as being opaque and keep instances around. This way the code is still
correct but (obviously) incomplete for polymorphic definitions and we
avoid introducing an anomaly. The patch does nothing clever, it only
keeps around instances with constants/inductives and compile constant
bodies only for non-polymorphic definitions.
|
|
constr for primitive records (not used anywhere else than printing).
Problem reported by P. LeFanu Lumsdaine on HoTT/HoTT.
Also add some minor fixes in detyping and pretty printing related to universes.
|
|
|
|
incompatibilities wrt 8.4.", as it creates other problems (in Ergo and
Compcert).
This reverts commit bf388dfec041ab0fa74ae5d484600f6fcf515e4f.
|
|
8.4.
|
|
|
|
typed-based matching: it provokes a stack overflow in contrib
ClassicalRealisability. To be investigated later on.
(See 893a02f643858ba0b0172648e77af9ccb65f03df.)
|
|
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.
|
|
|
