| Age | Commit message (Collapse) | Author |
|---|
|
The patch is done in a minimal way. The hacks are turned into a new kind of
safer hacks, but hacks nonetheless. They should go away at some point, but
the current patch is focussed on the removal of Libobject cruft, not making
the dirty code of its upper-layer callers any cleaner.
|
|
Reviewed-by: ppedrot
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
PR #9725 fixes completness bugs introduces some inefficiency. The
current PR intends to fix the inefficiency while retaining
completness. The fix removes a pre-processing step and instead relies
on a more elaborate proof format introducing positivity constraints on
the fly.
Solve bootstrapping issues: RMicromega <-> Rbase <-> lia.
Fixes #11063 and fixes #11242 and fixes #11270
|
|
There are no users in Coq but maybe some plugin wants it so don't
completely remove it
|
|
|
|
This was just dead code.
|
|
Some calls are actually guarded by a check that the scheme is already in
the cache. There is no reason to generate dummy side-effects in that case.
|
|
Fixes #10971
|
|
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Failing on CProdN([],...) was maybe a bit too radical.
|
|
Reviewed-by: ppedrot
|
|
The manual was already saying that it was deprecated, but no warning was
emitted.
Fixes #10572
|
|
Reviewed-by: ppedrot
|
|
library
Reviewed-by: ejgallego
|
|
Reviewed-by: ppedrot
|
|
This lets us get rid of dummy proofview manips.
Simplifications based on [(tclUNIT foo >>= f) = f foo]
|
|
It was a no-op.
|
|
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.
|
|
The proposed replacements are not satisfying because they are more
complicated to use. Following the discussion in #8713, we decide to
remove the deprecation warning for these commands.
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
