| Age | Commit message (Collapse) | Author |
|---|
|
|
|
relation
Reviewed-by: gares
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
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.
|
|
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
|
|
* Fix the implementations and add tests
* Change shift from int63 to Z (was always used as a Z)
* Update FloatLemmas.v accordingly
Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
|
|
* Add a related test-suite in compare.v (generated by a bash script)
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
|
|
|
|
Flag -fexcess-precision=standard is not enough on x86_32
where -msse2 -mfpmath=sse is required (-msse is not enough)
to avoid double rounding issues in the VM.
Most floating-point operation are now implemented in C because OCaml
is suffering double rounding issues on x86_32 with 80 bits extended
precision registers used for floating-point values, causing double
rounding making floating-point arithmetic incorrect with respect to
its specification.
Add a runtime test for double roundings.
|
|
* map special floats to registered CRef's
* kernel/float64.mli: add {is_infinity, is_neg_infinity} functions
* kernel/float64.ml: Replace string_of_float with a safe pretty-printing function
Namely:
let to_string_raw f = Printf.sprintf "%.17g" f
let to_string f = if is_nan f then "nan" else to_string_raw f
Summary:
* printing a binary64 float in 17 decimal places and parsing it again
will yield the same float, e.g.:
let f1 = 1. +. (0x1p-53 +. 0x1p-105)
let f2 = float_of_string (to_string f1)
f1 = f2
* OCaml's string_of_float gives a sign to nan values which shouldn't be
displayed as all NaNs are considered equal here.
|
|
|
|
Tests are updated to include native computations.
|
|
|
|
|
|
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.
|
|
Tests are updated to include VM computations and check for double
rounding.
|
|
Add utility ldexp and frexp functions to prevent dealing with the shift of
ldshiftexp and frshiftexp everywhere.
Also move primitive integer tests to place all primitive tests in the
same directory.
|
|
(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
|
|
Ack-by: Zimmi48
Ack-by: cpitclaudel
Reviewed-by: ejgallego
|
|
Ack-by: SkySkimmer
Ack-by: proux01
Reviewed-by: vbgl
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: jfehrle
|
|
We reach the anomaly because we call check_fix on a surrounding
fixpoint from the pretyper, and the inner fix hasn't been checked.
Using whd_all isn't useful in the specific reported case but a case
where it's necessary can probably be crafted.
See also #11013
|
|
Reviewed-by: ppedrot
|
|
Noticed by coverage, test code by Gäetan Gilbert.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Ack-by: JasonGross
Reviewed-by: ejgallego
|
|
Close #4502
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Ack-by: herbelin
|
|
Add experimental "Show Proof" command to the toplevel that shadows
the current command in the parser (in coqtop and PG only).
Apply existing code to highlight diffs in the output
|
|
|
|
These tactics now work correctly with multisuccess tactics by wrapping
the tactic argument in `once`.
Fixes #10965
|
|
We implement a new type of "preterms" that represent untyped ASTs, corresponding
to glob_expr in the ML implementations. Ltac2 quotations inside notations are
provided with such preterms, and have to pretype them in order to do anything
of relevance with them.
|
|
|
|
I still don't know why it produces a Not_found instead of a regular
error in coqtop but let's forget about it.
|
|
extensionality
Ack-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: maximedenes
|
|
|
|
homotopy propositions and homotopy sets. Rename local variable R in test Nsatz, to avoid a name collision with the type of real numbers.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
the Ltac-substituted environment
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
dune-compiled Coq
Reviewed-by: gares
|
|
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
|
|
More precisely: The equivalent in #7288 (4dab4fc) to the former call
to ltac_interp_name_env was not done anymore when interpreting
uconstr's.
|
|
Ack-by: JasonGross
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
