| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: gares
|
|
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
```
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
Ack-by: Zimmi48
|
|
Add missing zify class instances for `Pos.pred_double`, `Pos.pred_N`,
`Pos.of_nat`, `Pos.add_carry`, `Pos.pow`, `Pos.square`, `Z.pow`, `Z.double`,
`Z.pred_double`, `Z.succ_double`, `Z.square`, `Z.div2`, `Z.quot2`, `isZero`, and
`isLeZero`. Instances for `isZero` and `isLeZero` are useful to provide new
zify instances by using Micromega tactics.
|
|
|
|
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.
|
|
relation
Reviewed-by: gares
|
|
(as suggested by @silene)
|
|
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
|
|
|
|
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.
|
|
|
|
(namely, [RewriteRelation]s beyond Equivalence ones)
Thanks to @CohenCyril for suggesting this enhancement
|
|
|
|
* Preserve the same behavior/interface but merge the two Module Types
(UNDER_EQ and) UNDER_REL.
* Remove the "Reflexive" argument in Under_rel.Under_rel
* Update plugin code (ssrfwd.ml) & Factor-out the main step
* Update the Hint (viz. apply over_rel_done => apply: over_rel_done)
* All the tests still pass!
Credits to @CohenCyril for suggesting this enhancement
|
|
|
|
extensionality
Ack-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: maximedenes
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
|
|
|
|
AFAICT the reasoning for introducing this function doesn't hold
anymore. This is needed for future refactorings that should make some
types private.
|
|
|
|
homotopy propositions and homotopy sets. Rename local variable R in test Nsatz, to avoid a name collision with the type of real numbers.
|
|
Reviewed-by: Zimmi48
Reviewed-by: amahboubi
|
|
Reviewed-by: vbgl
|
|
|
|
|
|
|
|
try/with->assert false
as suggested by @gares (the Not_found exc may be catched by coq/ssr otherwise).
|
|
- Fix reification of overloaded operators
(triggers convertibility checks with existing terms)
- Zify instances need not be in hnf
- Fix specification of bool operators
- Add (limited) support for comparison
fixes #10779
|
|
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
Resolve by consulting is_custom/find_custom.
|
|
Reviewed-by: JasonGross
Reviewed-by: gares
Ack-by: ppedrot
|
|
AFAICT there is no reason to use interp_open_constr
I used Evd.from_ctx to keep passing evar maps around but maybe we
should be passing ustates instead?
|
|
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
projections
Reviewed-by: fajb
|
|
- Specialised hash and equality functions.
Avoid collisions in extreme scenarios.
- Flags to disable the use of the caches.
fixes #10772
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
intropattern entry in #10239)
Reviewed-by: ppedrot
|
|
|
|
#10239).
The bug was introduced in #10239 which seems to have actually remained
half-done: "wit_intropattern" and "wit_simple_intropattern" did not
share the same representation of values (val_tag) but the code was
assuming (especially the code for "fresh") that this was shared.
We fix it by sharing the internal representation (`dyn` field in
Tacarg.make0) as suggested by @ppedrot in the discussion of #10239
(this allows also to simplify Taccoerce.is_intro_pattern).
|
