| Age | Commit message (Collapse) | Author |
|---|
|
For now it does not do anything but eventually it should be used to replace
the reliance on canonical names for dual kerpairs such as e.g. constants and
inductive types.
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: vbgl
Ack-by: JasonGross
Ack-by: jfehrle
Ack-by: silene
|
|
Reviewed-by: herbelin
|
|
|
|
Update doc/sphinx/addendum/micromega.rst
Co-authored-by: Jason Gross <jasongross9@gmail.com>
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
Update doc/sphinx/addendum/micromega.rst
Co-authored-by: Jason Gross <jasongross9@gmail.com>
Update theories/micromega/ZifyInt63.v
Co-authored-by: Jason Gross <jasongross9@gmail.com>
|
|
|
|
IMO it makes more sense this way, also it's more convenient if someone
wants to run the script locally.
|
|
Commit 56ff0c9 mangled the code claiming to make it tail-rec, but this is not
the case. In addition to make the code convoluted it also over-allocates for
nothing and breaks the write barrier for fun.
We simply rollback to the (slightly cleaned-up) previous code, that was simpler,
likely faster, and as much tail-rec as the one introduced in 56ff0c9.
|
|
Co-authored-by: Clément Pit-Claudel <clement.pitclaudel@live.com>
|
|
Reviewed-by: SkySkimmer
|
|
Opaque/Transparent
Reviewed-by: SkySkimmer
|
|
make
Reviewed-by: SkySkimmer
|
|
Reviewed-by: silene
|
|
Reviewed-by: SkySkimmer
|
|
record types not taken into account
Reviewed-by: SkySkimmer
|
|
documentation
Reviewed-by: Zimmi48
|
|
|
|
We don't give sense to pattern/binders in leftmost position.
|
|
We prevent notations involving binders (i.e. names or patterns) to be
used for printing in "match" patterns. The computation is done in
"has_no_binders_type", controlling uninterpretation.
|
|
Reviewed-by: gares
|
|
|
|
Reviewed-by: ppedrot
|
|
not an integer
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
Fixes implicit arguments from the body of a defined field not taken into account.
Get (a bit) more information for detection of SProp relevance in
implicitly-typed defined field. (It should be done at the very end of
the inference phase, though, because some evars may not yet be
instantiated.)
|
|
This shall be for Record fields consumption.
|
|
Reviewed-by: herbelin
Ack-by: SkySkimmer
|
|
|
|
Similar to `dependent induction`, report an error message for `dependent
destruction` saying that importing `Coq.Program.Equality` is required,
rather than failing at parsing time.
This is a small extension of #605 to cover dependent destruction as
well. Here I also put in some tests.
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
Reviewed-by: Zimmi48
|
|
Reviewed-by: ejgallego
Ack-by: SkySkimmer
|
|
We fix a clear coding mistake in
79bcf1c0a22e736c4e2cae3460c35b3d9fca9aa0 that forgot to update the
type of the parameter entry when saving mutual definitions without a
body.
We follow the solution suggested by Hugo Herbelin and drop the
type used in `start_proof`. Note the duplication here indeed.
Fixes #12895
Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
|
|
(zero references is currently a no-op)
|
|
integer
|
|
|
|
|
|
output path
In #11581 we introduced the `-native-output-dir` option to allow the
build system to redirect the output of the native compiler.
Unfortunately that patch also modified the default loadpath, which is
now buggy if a library with native is installed.
We thus revert the change to the loadpath handling, so for now
additional native build paths have to be passed with `-nI`.
Note that unfortunately in `link_library` we don't know if the
required library is coming from the build dir or from an installed
dir, as this information is generated from `Require` statements in
`Library.get_used_load_paths`. We thus check and give priority to
files in the build location.
As to make the patch backportable I introduced an extra `stat` system
call which should not be problematic as the cache will be hot for the
second call.
An alternative would be actually to modify loadpath compilation in
`call_compiler` so both include paths would be added if `output_dir`
is not the default, however that seems pretty noisy given the large
path set returned by `!get_load_paths`.
|
|
Fix #12970
We can't recover the expected type of the post bidi argument by
retyping because the hole may be filled by something in which case
retyping can produce algebraic universes.
|
|
Fix #13162
|
|
Note: "hyp" was documented in Ltac Notation chapter but "var" was not.
|
|
Reviewed-by: erikmd
Reviewed-by: silene
|
