| Age | Commit message (Collapse) | Author |
|---|
|
Workers send back incomplete system states (only the proof part).
Such part must include the meta/evar counter.
|
|
Should make the compilation of Coq more robust against LaTeX errors.
See e.g. #4091.
|
|
|
|
Due to the way it was laid out, the tactic could prove neither
(Zle x x) nor (P /\ Q -> P) nor (P |- P /\ True)
yet it could prove
(Zle x x /\ True) and (P /\ Q |- P).
|
|
|
|
ensure_evar_independent into is_constrainable_in (a simpler approach
closest to what existed before cf6a68b45).
|
|
|
|
inefficiency #4076.
In an evar context like this one
x:X, y:=f(x), z:Z(x,y) |- ?x : T(x,y,z)
with unification problem
a:A, b:=f(t(a)) |- ?x[x:=t(a);y:=b;z:=u(a,b)] = v(a,b,c)
we now keep y after filtering, iff the name b occurs effectively in
v(a,b,c), while before, we kept it as soon as its expansion f(t(a))
had free variables in v(a,b,c), which was more often, but useless
since the point in keeping a let-in in the instance is precisely to
reuse the name of the let-in while unifying with a right-hand side
which mentions this name.
|
|
|
|
of plugins.
|
|
progress.
Also compare goals up to evar instantiation (otherwise no progress would be observed when only unification occurs, unless some [nf_evar] is done). Performance look unchanged so far.
Some code from [Evd] which was used only in [tclPROGRESS] have been moved out (and [progress_evar_map] was now dead, so I killed it).
Fixes bugs (one reported directly on coqdev, and #3412).
|
|
[kind_of_term].
To be able to write equality up to evar instantiation instantiation.
Generalises the main function of [eq] constr over the variant of [kind_of_term] it uses. It prevents some optimisation of [Array.equal] where two physically equal arrays are considered (less or) equal. But it does not seem to have appreciable effects on efficiency.
|
|
[compare_head_gen] defined in terms of [compare_head_gen_leq]. Remove an unused argument from [compare_head_gen_leq].
|
|
|
|
Since they don't work anymore.
|
|
|
|
integrating ensure_evar_independent into is_constrainable_in.
|
|
Also make uninstall_me.sh a real target with proper dependencies.
|
|
Fixes bug #4089.
|
|
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.
|
|
|
|
fresh now accepts a qualid, and behaves as if given the short name.
Since fresh used to accept an id, supporting qualid is IMO not a new
feature but just a fix. Hence the fix in v8.5.
|
|
|
|
|
|
|
|
|
|
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?
|
|
|
|
(thanks to Enrico for noticing a bug).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Instead of registering all the transitive dependencies of a term in one go,
we rather recursively build the graph of direct dependencies of this term.
This is finer-grained and offers a better API.
The traversal now uses the standard term fold operation, and also registers
inductives and constructors encountered in the traversal.
|
|
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].
|
|
help).
|
|
|
|
|
|
|
|
|
|
|
