| Age | Commit message (Collapse) | Author |
|---|
|
|
|
and do not run template_candidate in the upper layers when the
template attribute is given.
This means we can use an over-approximation in the upper layer
implementation of template_candidate (returning false even in cases
which the kernel may accept) if we ever want to.
|
|
Using the parameter universes in the constructor causes implicit
equality constraints, so those universes may not be template
polymorphic.
A couple types in the stdlib were erroneously marked template, which
is now detected. Removing the marking doesn't actually change
behaviour though.
Also fixes #10504.
|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
cleaning
Reviewed-by: ejgallego
|
|
Reviewed-by: gares
Reviewed-by: silene
|
|
"similar" means sharing a scope or implicit status.
|
|
ie keep the fake arguments "/" and "&" instead of getting their index
at parsing time.
|
|
(fixing bug #11057).
With this new behavior, it is not needed to .vos files in user contribs.
Also, this commit adds a feature: upon creation of a .vo file, an empty .vok file is touched.
|
|
This is in accordance with PR #10614 and to avoid a confusion with the
fields of a record type in g_vernac.ml.
Removing a useless line at the same time in G_vernac.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
Ack-by: Zimmi48
Ack-by: herbelin
|
|
|
|
not sure what that's about
|
|
We can now do `#[refine] Instance : Bla := bli.` to enter proof mode
with `bli` as a starting refinement.
If `bli` is enough to define the instance we still enter proof mode,
keeping things nicely predictable for the stm.
|
|
|
|
Ack-by: Blaisorblade
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
This should ideally have been done before the 8.11 branching.
|
|
Reviewed-by: ppedrot
|
|
This means return_proof is the only place where it can be produced.
We need to change the stm a bit as it keeps a pointer to a
[closed_proof_output] to join and to check if it failed, and it needs
a way to create a dummy in 1 case.
I'm not sure if this works correctly though, how to test?
We also inline the used bits of [return_proof ~allow_partial:true] in
[save_lemma_admitted] to get [Proof using] info. We could
alternatively expose the [closed_proof_output -> constr list]
projection. I think the code is easier to understand this way though,
as we don't have to read [return_proof] and figure out that the side
effect manipulation is ignored etc.
Note that the "this will warn" comment was outdated since
73daf37ccc7a44cd29c9b67405111756c75cb26a
|
|
Reduction.whd_all does not commute with to_constr.
|
|
This probably does not work well in general, and specifically avoids
an anomaly fixing https://github.com/coq/coq/issues/10060
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl
|
|
|
|
|
|
A .vos file stores the result of compiling statements (defs, lemmas)
but not proofs.
A .vok file is an empty file that denotes successful compilation of
the full contents of a .v file.
Unlike a .vio file, a .vos file does not store suspended proofs,
so it is more lightweight. It cannot be completed into a .vo file.
|
|
* Add a related test-suite in compare.v (generated by a bash script)
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
|
|
|
|
|
|
Replace `option comparison` with `float_comparison` (:= `FEq | FLt |
FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid
boxing and an extra match when using primitive float comparison.
|
|
Beware of 0. = -0. issue for primitive floats
The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
|
|
Rather than in typeops
|
|
Ack-by: Zimmi48
Ack-by: cpitclaudel
Reviewed-by: ejgallego
|
|
`Prettyp` is now late enough in linking to refer to them.
|
|
system
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
|
|
|
|
Close #10961
|
|
|
|
|
|
Suggested by Gaëtan Gilbert.
|
|
|
|
Note the ugly problem that we have on close_proof:
```
proof_global.ml:278
let entry_fn p (_, t) =
let t = EConstr.Unsafe.to_constr t in
let univstyp, body = make_body t p in
```
arguments of start_proof should be pre-normalized.
I think this will require a lot of refactoring to be fixed properly.
|
|
|
|
This means we can disable it to ignore unsupported attributes. For
instance this would be useful if we change some behaviour of `Cmd` and add an
attribute `att` to restore the old behaviour, then `#[att] Cmd` is
backwards compatible if the warning is disabled.
|
|
Reviewed-by: ejgallego
|
