| Age | Commit message (Collapse) | Author |
|---|
|
That release includes non trivial changes related C compilers, in
particular due to `-fno-common` support.
|
|
Reviewed-by: JasonGross
Ack-by: SkySkimmer
|
|
|
|
That is, it contains the type of the binder so as not to rely on the relevance
explicitly.
|
|
For robustness and it is better to leave it opaque. Users are not supposed to
fiddle with it.
|
|
Reviewed-by: jfehrle
|
|
Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: maximedenes
|
|
Reviewed-by: ppedrot
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
|
|
|
|
Cf. discussion at #11559 and decision of Coq Call 2020-02-26.
|
|
We reuse the same type as for options, even though it is a bit ill-named. At
least it allows to share code with it.
|
|
The current implementation was seemingly never thought for this kind of
semantics. Everything is superglobal by construction, notably hint database
creation and naming schemes. The new mode feels a bit hackish to me, at
some point this should be fully reimplemented from scratch with a clear
design in mind.
|
|
plugins (e.g. gappa)
Reviewed-by: Zimmi48
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
|
|
We bump ounit, odoc, and lablgtk3 ; so far this is routine maintenance.
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
|
|
VST has been fixed upstream, c.f.
https://github.com/PrincetonUniversity/VST/issues/392
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
|
|
Ack-by: ejgallego
|
|
is contiguous to the number.
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
A constraint can be stuck if it does not match any of the declared modes
for its head (if there are any). In that case, the subgoal is postponed
and the next ones are tried. We do a fixed point computation until there
are no stuck subgoals or the set does not change (it is impossible to
make it grow, as asserted in the code, because it is always a subset of
the initial goals)
This allows constraints on classes with modes to be treated as if they were
in any order (yay for stability of solutions!). Also, ultimately it should
free us to launch resolutions more agressively (avoiding issues like the
ones seen in PR #10762).
Add more examples of the semantics of TC resolution with apply in test-suite
Properly catch ModeMatchFailure on calls to map_e*
Add fixed bug 9058 to the test-suite
Close #9058
Add documentation
Fixes after Gaëtan's review.
Main change is to not use exceptions for control-flow
Update tactics/class_tactics.ml
Clearer and more efficient mode mismatch dispatch
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Remove exninfo argument
|
|
10.13 is deprecated as an azure VM
Close #11449
|
|
>= 4.08 (#11624)
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Now that `MutualEntry` provides a more uniform interface we can reuse
`Info.t`
In the medium term we shall consolidate `Proof` / `Proof_global` and
`Lemmas` so admitted / finish are uniform too.
|
|
In preparation for the introduction of an opaque mutual definition
type at the `Declare` level we remove the not very useful wrapper
`declare_fix`.
Now we should be ready to profit from `DeclareDef` and its handling of
common stuff such as `restrict_universe_context` and `check_univ_decl`
etc...
|
|
We split the paths for mutual / non-mutual constants, and we enforce
some further invariants, in particular we avoid messing around with
the body of saved constants, and using the indirect accessor.
This should be almost semantically equivalent to the previous code,
including some questionable choices present there.
In further cleanups we will move this code to Declare, which should
hopefully help clarify some of the semantics.
|
|
As suggested by Gaëtan in review, we move declaration of universe
binders to the common code in `DeclareDef`; this changes the semantics
for the assumption case when Recthms is not empty.
|
|
We move towards more unification in the proof save path of interactive
and non-interactive proofs.
|
|
|
|
|
|
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
and removed the now incorrect "section 8.2.3" reference, as it is the same as the "refine" link.
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: cpitclaudel
|
