| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: jfehrle
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
|
|
This change improves the relaxed ambiguous path condition of coercions (#9743)
to check that any circular inheritance path of `C >-> C` is definitionally equal
to the identity function of the class `C`. Moreover, for a new inheritance path
`p : C >-> D` and existing (valid) one `q : C >-> D`, the new mechanism does not
report the ambiguity of `p` and `q` if they have a common element, that is to
say:
`p = p1 @ [c] @ p2` and `q = q1 @ [c] @ q2`
for some coercion `c` and inheritance paths `p1`, `p2`, `q1`, and `q2`.
In that case, convertibility of `p1` and `q1`, also, `p2` and `q2` should be
checked; thus, checking the ambiguity of `p` and `q` is redundant with them.
If the new mechanism does not report any ambiguous path, the inheritance graph
must be coherent [Barthe 1995, Sect. 3.2] [Saïbi 1997, Sect. 7]:
1. for any circular path `p : C >-> C`, `p` is definitionally equal to the
identity function, and
2. for any two paths `p, q : C >-> D`, `p` and `q` are convertible.
[Barthe 1995] Gilles Barthe, Implicit coercions in type systems, In: TYPES '95,
LNCS, vol 1158, Springer, 1996, pp 1-15.
[Saïbi 1997] Amokrane Saïbi, Typing algorithm in type theory with inheritance,
In: POPL '97, ACM, 1997, pp 292-301.
|
|
Check that we don't regress on PR #10762 example
Fix regression discovered by Arthur in PR #10762
Fix script of #10298 which was relying on breaking semantics for `eapply`
Add doc
Add comment in clenvtac
Actually, always mark shelved goals as unresolvable
Update doc to reflect semantics w.r.t. shelved subgoals
|
|
This is the minimal set of changes requires for Coq to build under 2.0
mode. We may likely take advantage of some more new features.
Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune
in older versions as it will install a secondary compiler.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: silene
|
|
Reviewed-by: SkySkimmer
Reviewed-by: cpitclaudel
|
|
The manual was already saying that it was deprecated, but no warning was
emitted.
Fixes #10572
|
|
|
|
|
|
|
|
|
|
This increases backwards compatibility. If desired, we can add a tactic
notation to simplify the spec of `rapply` in the future if we want.
|
|
Also add a tactic notation so that it takes in uconstrs by default.
Also add some basic tests for `rapply`.
Also document rapply in the manual
|
|
Close #9634
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Ack-by: Zimmi48
|
|
|
|
Reviewed-by: gares
Reviewed-by: silene
|
|
Update doc_grammar tool
The grammar in the doc is generated semi-automatically with doc_grammar:
- the grammar is automatically extracted from the mlg files
- developer-prepared editing scripts *.mlg_edit modify the extracted
grammar for clarity, simplicity and ordering of productions
- chunks of the resulting grammar are automatically inserted into the
rsts using instructions embedded in the rsts
Running doc_grammar is currently a manual step.
The grammar updates in the rst files have been manually reviewed.
|
|
Reviewed-by: cpitclaudel
|
|
(fixing bug #11057).
With this new behavior, it is not needed to .vos files in user contribs.
Also, this commit adds a feature: upon creation of a .vo file, an empty .vok file is touched.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
Fix #10570
|
|
Reviewed-by: Zimmi48
Ack-by: cpitclaudel
|
|
|
|
This documentation seems to have been lost after it was introduced by
0ad26633a4589d77de1f864733d1d953dab9ea91
We also document that this flag is deprecated.
|
|
Only the deprecated one was documentated, and the deprecation was not
mentioned.
|
|
We can now do `#[refine] Instance : Bla := bli.` to enter proof mode
with `bli` as a starting refinement.
If `bli` is enough to define the instance we still enter proof mode,
keeping things nicely predictable for the stm.
|
|
Reviewed-by: Zimmi48
|
|
|
|
Close #10242
|
|
@eelcovisser told me that the strategies in Luttik and Visser 97 were inspired
by Elan, but they are not part of Elan. They are part of the Stratego language.
|
|
|
|
relation
Reviewed-by: gares
|
|
Now it uses `.. deprecated` like all the other deprecation notices in
the manual.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl
|
|
|
|
|
