| Age | Commit message (Collapse) | Author |
|---|
|
cleanall
Reviewed-by: gares
|
|
|
|
- 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.
|
|
While we're at it also compare instances in glob_constr although I
don't know if that changes any behaviour.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: mattam82
|
|
Reviewed-by: ejgallego
|
|
starting emphasis.
This is to support referring to names such as _CoqProject.
|
|
|
|
The location was missing in the parser.
|
|
coqdoc.
|
|
In particular, the error messages do not mention anymore the notion of
bool-valued options, since these are documented as flags and work
quite differently from the rest of options.
|
|
|
|
|
|
|
|
It seems that this PR is making the rewrite much, much faster.
|
|
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.
|
|
There is no point in using the exaggerately inefficient Reductionops machine.
We need to be call-by-name to preserve the shape of the reduced terms, as
call-by-need would introduce sharing and thus at-distance effects in term
refolding. Yet, the Reductionops machine is worse than that, since it performs
substitutions eagerly, leading to a catastrophical performance profile.
Instead, we use the kernel reduction in by-name mode to replace the Reductionops
machine in whd_betaiota_deltazeta_for_iota_state with all flags on. Since the
kernel is using explicit substitutions, this is algorithmically more efficient.
Apart from minor differences, this should produce the same normal form.
As showed by the benchmarks, this is a critical change for the odd-order proofs.
Ideally, we should use delayed substitutions in the Reductionops machine as well
for great profit, but due to code entanglement this is a much less self-contained
change.
|
|
Reviewed-by: ejgallego
|
|
autogen.sh was removed in https://gitlab.inria.fr/flocq/flocq/-/commit/d679d3770aea2ff8608c77096158653837798124
|
|
parsing of coqtop arguments in coqide
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: jfehrle
|
|
This octopus merge is meant to preserve the commit history / blame of
all the parts.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
gallina-ext chapter.
|
|
|
|
|
|
|
|
The idea is very simple: use the list in the release branch to know
which changelog entries to include, but do the work of removing these
entries and consolidating the released changelog in the master branch
(so that it is applied both to the master branch and to the release
branch following the backporting process).
|
|
Reviewed-by: Zimmi48
|
|
Auto-generated files like the Makefile have recently been removed from
the sources (cf. coq-community/corn#88). Calling ./configure.sh is
now required.
|
|
|
|
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Reviewed-by: anton-trunov
|
|
Reviewed-by: cpitclaudel
|
|
So far it was only documented in coqtop --help.
|
|
|
|
|
|
|
|
|
|
This option is confusing because it does Require Import, not Require.
It was deprecated in 8.11. We remove it in 8.12 in order to
reintroduce it in 8.13 as a replacement for -load-vernac-object, which
is the option that does Require without Import as of today.
|
|
We try to consistently register inductive types defined in the
[Coq.Init.Datatypes] module, so that they can be fetch using
[Coqlib.ref_lib]. We follow a naming scheme consistent with the rest
of the module, that is: `core.<type name>.type' for the type, and
`core.<type name>.<constructor name>' for the constructors.
|
|
Reviewed-by: ppedrot
|
|
This was an undocumented equivalent of the Section command.
|
