| Age | Commit message (Collapse) | Author |
|---|
|
Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g.,
`Opaque foo` doesn't break some automation which tries to unfold `foo`.
We have some timeouts in the strategy success file. We should not run
into issues, because we are not really testing how long these take. We
could just as well use `Timeout 60` or longer, we just want to make sure
the file dies more quickly rather than taking over 10^100 steps.
Note that this tactic does not play well with `abstract`; I have a
potentially controversial change that fixes this issue.
One of the lines in the doc comes from
https://github.com/coq/coq/pull/12129#issuecomment-619771556
Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>
Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr>
Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
Reviewed-by: ppedrot
|
|
line -sprop-cumulative
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
NB: 3 dots doesn't play well with PG's sentence detection.
|
|
This is a critical warning in terms of future compatibility but it
makes no sense to be verbose about it every build.
|
|
|
|
Reviewed-by: ppedrot
|
|
Being able to inspect the generated OCaml code is a useful debug tool.
It seems this was disabled by mistake in #11081.
|
|
- Provide new helper functions in `Goptions` on the model of
`declare_bool_option_and_ref`;
- Use these helper functions in many parts of the code base
(encapsulates the corresponding references);
- Move almost all options from `declare_string_option` to
`declare_stringopt_option` (only "Warnings" continue to use the
former). This means that these options now support `Unset` to get
back to the default setting. Note that there is a naming
misalignment since `declare_int_option` is similar to
`declare_stringopt_option` and supports `Unset`. When "Warning" is
eventually migrated to support `Unset` as well, we can remove
`declare_string_option` and rename `declare_stringopt_option` to
`declare_string_option`.
- For some vernac options and flags that have an equivalent
command-line option or flag, implement it like the standard `-set`
and `-unset`.
|
|
This corresponds more naturally to the use we make of them, as we don't need
fast indexation but we instead keep pushing terms on top of them.
|
|
A quick analysis showed that most of the calls to whd do not lead to a
term which further triggers reduction, so there is no point in refolding
a potentiall huge term for no reason.
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: erikmd
|
|
|
|
than our own.
Ack-by: aaronpuchert
Ack-by: gadmm
Reviewed-by: maximedenes
Ack-by: ppedrot
Reviewed-by: proux01
|
|
|
|
For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
|
|
|
|
This module used to do retyping for the kernel in prototypes of SProp,
but was switched to only relevance inference before the merge.
|
|
Add headers to a few files which were missing them.
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
Reviewed-by: SkySkimmer
|
|
This commit also prefixes young_ptr and young_limit along the way, so as
to not rely on OCaml's compatibility layer. This is a gratuitous change,
since this code is only meant to be compiled with OCaml < 4.10 anyway.
|
|
This could have been at the root of strange behaviours (read unsoundness).
|
|
For an inductive block to be template, all its components must also
be. This is probably fixing a few soundness bugs in the process, but I
do not want to think too much about it.
|
|
We also factorize a few checks by returning an option when looking for
a potentially template universe.
|
|
Cleanup: IMHO most of the re-raises here are not worth it.
|
|
|
|
|
|
|
|
The current behaviour could be considered as sub-optimal, but it probably
doesn't matter in practice as this happens when serializing side-effects.
|
|
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
|
|
`Nativelib` currently assumes that objects are built in some
particular directories, but this is not true in some cases, for
example, when building with Dune.
We add a new option `-nI` to allow clients to specify the OCaml
include dirs.
|
|
This is useful in order to implement native support in Dune for
example, which as of today as strict target rules.
Hopefully this option could go away; it is really internal, but I've
chosen to document it.
|
|
Apart from being an ugly hack in the kernel, the universe-adding function
is already robust to redundant universes anyways.
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
