| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
In practice, this is almost invisible except when using "refine". So,
in some sense, it is aligning the behavior of pretyping on the one of
logic.ml's "refine" so that the more natural behavior of 8.4's refine
on this issue is restored.
|
|
pattern-matching for refine.
|
|
There is a long story of commits trying to improve the compatibility
between 8.4 and 8.5 refine, as discussed in
https://github.com/coq/coq/pull/346.
ac9c5986b77bf4a783f2bd0ad571645694c960e1 add beta-iota in hypotheses and conclusion
8afac4f87d9d7e3add1c19485f475bd2207bfde7 remove beta-iota in hypotheses
08e87eb96ab67ead60d92394eec6066d9b52e55e re-add beta-iota in hypotheses
c9c54122d1d9493a965b483939e119d52121d5a6 re-remove beta-iota in hypotheses
9194180e2da0f7f9a2b2c7574bb7261cc69ead17 revert re-remove beta-iota in hypotheses
6bb352a6743c7332b9715ac15e95c806a58d101c re-re-remove beta-iota in hypotheses if <= 8.5
d8baa76d86eaa691a5386669596a6004bb44bb7a idem if = 8.5
The current commit tries to identify (one of?) the exact points of
divergence between 8.4 and 8.5 refine, namely the types inferred for
the variables of a pattern-matching problem.
Note that for the conclusion of each new goal, there were a
nf_betaiota in 8.4 done in function Evarutil.evars_to_metas, so the
compatibility expects that such a nf_betaiota on the conclusion of
each goal remains.
|
|
|
|
|
|
|
|
We export the relevant level equality function in UGraph which is way faster
than checking that each one is smaller than the other as universes.
|
|
This patch is only moving code around and expliciting statically the
invariants of the functions, so it should be 1:1 equivalent to the other
one. Amongst other goodies, the unification function is not recursive
anymore, which ensures that it will terminate.
|
|
|
|
|
|
|
|
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.
|
|
As per Enrico's request.
|
|
|
|
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.
|
|
No need to use `discriminate`. This is the hopefully uncontroversial part of https://github.com/coq/coq/pull/401.
|
|
|
|
This is a partial backtrack on
63cfc77ddf3586262d905dc351b58669d185a55e. In that commit, we
disregarded exception and tried to print error messages just by
listening to feedback.
However, feedback error messages are not always emitted due to
https://coq.inria.fr/bugs/show_bug.cgi?id=5479
Thus meanwhile it is safer to go back to printing the information
present in exceptions until we tweak the STM.
This fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5467 and many
other glitches not reported, such errors in nested proofs.
|
|
|
|
Due to code reworking, a fastpath got anihilated because the slow path
was computed altogether. We now only compute the slow check whenever the
quick one fails.
|
|
Due to code reworking, a fastpath got anihilated because the slow path
was computed altogether. We now only compute the slow check whenever the
quick one fails.
|
|
|
|
|
|
|
|
We remove some unnecessary functions introduced before in the patch
series + unused functions.
|
|
|
|
Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.
This provides significantly clearer code for the AST, and is robust
wrt attributes.
|
|
Thanks to @gasche
|
|
|
|
`internal_ghost` was an artifact to ease porting of the ml4 rules. Now
that the location is optional we can finally get rid of it.
|
|
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.
|
|
One case missing due the TACTIC EXTEND macro.
|
|
|
