| Age | Commit message (Collapse) | Author |
|---|
|
This should save us a lot of useless hashconsing. This change should not be
observable because outside of the proof, the abstracted definition will be
either inlined or redefined with the body coming from the side-effect.
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: silene
|
|
Close #12909
|
|
Reviewed-by: mattam82
Ack-by: ppedrot
|
|
Fix #7015
|
|
|
|
|
|
This is not pretty but I do not see how to do this in a way that is both
backwards compatible and efficient.
|
|
Reviewed-by: SkySkimmer
Ack-by: silene
|
|
No need to store the case_info, all the data is reconstructible from the
context. Furthermore, this reconstruction is performed in a context where
we already access the environment, so performance is not at stake.
Hopefully this will also reduce the number of globally allocated VM values,
since the switch representation now only depends on the shape of the inductive
type.
|
|
|
|
The default value of the delta-resolver for name aliasing was
reinitialized at Module and Module Type starting time. The existing
resolver was saved but the saved value was not used in
Safe_typing.constant_of_delta_kn_senv and
Safe_typing.mind_of_delta_kn_senv.
A possible fix could have been to take the saved resolver into account
in Safe_typing.constant_of_delta_kn_senv and
Safe_typing.mind_of_delta_kn_senv. We just try instead not to
reinitialize it.
This incidentally fixes #12525 (Search unable to see through an
"Include" when in an ongoing "Module").
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Instead of costly linear reallocations, we share as much as possible of the
prefixes of the various environment subcomponents.
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
|
|
Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.
I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.
There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...
|
|
This makes the invariants in the code clearer, and also highlight this is
only required to implement template polymorphic inductive types.
|
|
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.
|
