| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |/ / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which
this PR solves, I propose to remove support for non-synchronous
options.
It seems the few uses of `optsync = false` we legacy and shouldn't
have any impact.
Moreover, non synchronous options may create particularly tricky
situations as for instance, they won't be propagated to workers.
|
| | | | | |
|
| | | |/
| |/|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We do that by using constr_with_bindings rather than
open_constr_with_bindings (+ extra call to typeclasses in
"specialize"). If my understanding is right, the only effect would be
to succeed more in cases where it was failing (in
inh_conv_coerce_to_gen). In particular, "specialize" and
"contradiction" already have a WITHHOLES test for rejecting pending
holes.
Incidentally, this answers enhancement #5153.
|
| | |\ \ |
|
| | | | |\ |
|
| | | |_|/
| |/| |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
With the "apply in" introduction pattern, and the backtrack possibly
done in "apply" over the components of conjunctions
(descend_in_conjunctions), the reasons for failing might have
different sources.
We give priority to the detection of used names over other
(unification) errors so that an error there is not masked in the
backtracking made by descend_in_conjunctions.
Of course, the question of what best unification error to give in the
presence of backtracking is still open.
|
| | |/ / |
|
| | |\ \ |
|
| | | | | |
|
| | | | | |
|
| | |\ \ \ |
|
| | | | | | |
|
| | |\ \ \ \ |
|
| | | | | | | |
|
| | | |_|_|/
| |/| | | |
|
| | |\ \ \ \ |
|
| | | | | | | |
|
| | |\ \ \ \ \ |
|
| | |\ \ \ \ \ \ |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
- Fixing a typo introduced in 31dbba5f.
- Adapting to computation of universe constraints in pretyping.
- Adding a regression test.
|
| | | | | | | | | |
|
| | | |_|_|/ / /
| |/| | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Since 260965d, an imperative code was semantically the identity because the
closure allocation was not performed at the right moment. Because of it
intricacy, I cannot really tell the original motivations of this piece of
code, although it looks like it was for there for pretty-printing of errors.
Anyway, both because the code was dubious and its effect not observed, it
cannot hurt to remove it.
|
| | | |/ / / /
| |/| | | |
| | | | | |
| | | | | | |
A universe substitution was lacking as the normalized evar map was dropped.
|
| | | |/ / /
| |/| | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The code was assuming that the terms t and u for which {t=u}+{t<>u} is
proved were distinct. We refine an internal "generalize" of "u" so
that it works on the two precise occurrences to abstract, even if
other occurrences of u occur as subterm of t too.
We also reuse the global constants found in the statement rather than
reconstructing them (this seems better in case the global constants
eventually get polymorphic universes?).
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
I'm sure this was pushed by accident, since testing shows immediately
that it breaks the compilation of the ssreflect plugin, hence all
developments relying on it in Travis.
|
| | | | | |
| | | | |
| | | | |
| | | | | |
A priori considered to be a good programming style.
|
| | |\ \ \ \
| | | | | |
| | | | | |
| | | | | | |
let-ins
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | |/ / /
| |/| | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
https://github.com/coq/coq/pull/201#discussion_r110957570
|
| | | | | |
| | | | |
| | | | |
| | | | | |
https://github.com/coq/coq/pull/201#discussion_r110952601
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Also move named arguments to the beginning of the functions. As per
https://github.com/coq/coq/pull/201#discussion_r110928302
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This will allow a cache_term tactic that doesn't suffer from the
Not_found anomalies of abstract in typeclass resolution.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This is a small change that allows a transparent version of tclABSTRACT.
Additionally, it factors the machinery of [abstract] through a
plugin-accessible function which allows alternate continuations (other
than exact_no_check.
It might be nice to factor it further, into a cache_term function that
caches a term, and a separate bit that calls cache_term with the result
of running the tactic.
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
|
| | | | | |
| | | | |
| | | | |
| | | | | |
Now it is a private field, locations are optional.
|
| | |_|/ /
|/| | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The current implementation was still using continuation passing-style, and
furthermore was triggering a focus on the goals. We take advantage of the
tactic features instead.
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The only remaining use was applied on the unfold tactic, and the behaviours
of tclPROGRESS and tclWEAK_PROGRESS coincide whenever only one goal is produced
by their argument tactic.
|
Maxime Dénès
Emilio Jesus Gallego Arias
Hugo Herbelin
Pierre-Marie Pédrot
Théo Zimmermann
Gaetan Gilbert
Jason Gross