| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
|
|
Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.
As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.
|
|
|
|
This is actually not so perfect because of the lambdas in the return
clause which we would not like to look in.
|
|
for being able to interpret a "match" as a constr pattern).
|
|
|
|
|
|
removing all evars appearing in the constr (or their types,
recursively) from the evar_map.
|
|
QuicksortComplexity).
|
|
|
|
|
|
The context matching function was dropping the surrounding context in
let-ins.
|
|
for which there corresponding tag are greater than max_variant_tag.
The code is a merge with the patch proposed by Bruno on
github barras/coq
commit/504c753d7bb104ff4453fa0ede21c870ae2bb00c
|
|
change the representation of inductive constructor
when there is too many non constant constructors in the inductive type
Conflicts:
kernel/cbytegen.ml
|
|
presence of let-ins and recursively non-uniform parameters).
The bug was in the List.chop of Inductiveops.get_arity which was wrong
in the presence of let-ins and recursively non-uniform parameters.
The bug #3491 showed up because, in addition to have let-ins, it was
wrongly detected as having recursively non-uniform parameters.
Also added some comments in declarations.mli.
|
|
bug #4133)
Note that, if someone was purposely modifying the user name of a type in
order to disable a coercion, it no longer works. Hopefully, no one did.
|
|
|
|
|
|
|
|
unification fails due to that, during a conversion step.
|
|
pattern_of_constr in an evar_map, as they can appear in the context
of said named metas, which is used by change. Not sure what to do in
the PEvar case, which never matches anyway according to Constr_matching.matches.
|
|
cases, in some cases.
|
|
when called from w_unify, so we protect it.
|
|
index lookup.
|
|
|
|
|
|
as revealed by #2141).
|
|
It was an integer overflow! All sorts of memories.
|
|
is reduced as if without let-in, when applied to arguments.
This allows e.g. to have a head-betazeta-reduced goal in the following example.
Inductive Foo : let X := Set in X := I : Foo.
Definition foo (x : Foo) : x = x. destruct x. (* or case x, etc. *)
|
|
clause in the presence of let-ins in the arity of inductive type).
|
|
inductive types with let-in in arity.
|
|
together with the tactic monad.
The move is not complete yet, because some file candidates for this directory
have almost useless dependencies in other ones that should not be moved.
|
|
Workers send back incomplete system states (only the proof part).
Such part must include the meta/evar counter.
|
|
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.
|
|
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).
|
|
integrating ensure_evar_independent into is_constrainable_in.
|
|
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.
|
|
|
