| Age | Commit message (Collapse) | Author |
|---|
|
This encodes/decodes a list of string into a string in a way
compatible with shell interpretation. On the contrary of
Filename.quote which is for computer consumption, it introduces quotes
for human consumption.
The strategy is to split each string into substrings separated by
simple quotes. Each substring is surrounted by single quotes if it
contains a space. Otherwise, each backslash in the substring is
doubled. The substrings are concatenated separated by
backslash-protected single quote. The strings are then concatenated
separated with spaces. The decoding is shell-like in the sense that it
follows the rules of single quote, backslash and space.
|
|
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.
|
|
|
|
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: cpitclaudel
|
|
Reviewed-by: cpitclaudel
|
|
Reviewed-by: Zimmi48
|
|
|
|
Closes #11758
It turns out that we were overwriting the default `ocamlopt_flags`,
thus creating a problem in the release build.
|
|
Ack-by: SkySkimmer
Reviewed-by: fajb
|
|
Reviewed-by: SkySkimmer
|
|
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
VST has been broken for a few days, moving to allow failure.
|
|
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
|
there is an ocamlopt compiler.
|
|
compiler. In any case, try to build a cmo file.
|
|
open.
Reviewed-by: MSoegtropIMC
|
|
Since version 1.0.0 of the sphinxcontrib-bibtex extension, parallel
building of the Sphinx documentation emits a warning (and thus makes
our warning-free build fail).
This change was already done in Makefile.doc as part of #11732.
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: ppedrot
Reviewed-by: proux01
|
|
|
|
We are using some Sphinx extensions that are not safe w.r.t. parallel
reaading.
|
|
|
|
This is only used in `Ccalgo` and it does not provide any advantage
these days over the upstream OCaml implementation.
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
|
|
Ack-by: Zimmi48
|
