| Age | Commit message (Collapse) | Author |
|---|
|
In particular, display how long they took in bogomips-adjusted
centiseconds.
|
|
|
|
universes
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
Reviewed-by: herbelin
|
|
This increases backwards compatibility. If desired, we can add a tactic
notation to simplify the spec of `rapply` in the future if we want.
|
|
Also add a tactic notation so that it takes in uconstrs by default.
Also add some basic tests for `rapply`.
Also document rapply in the manual
|
|
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
|
|
refined version of #8890 which prevents #11033.
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
|
|
Reviewed-by: ejgallego
|
|
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
|
|
|
|
This is to hopefully prevent regressions on
https://github.com/coq/coq/issues/11150 and
https://github.com/coq/coq/issues/6502.
|
|
This is better than expecting other tests to fail if we mess up again.
|
|
We restrict #8890 so that it looks for a notation only for the fully
applied coercion.
|
|
`Fixpoint` with a let binder
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Reviewed-by: gares
Reviewed-by: silene
|
|
"similar" means sharing a scope or implicit status.
|
|
(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.
|
|
|
|
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.
|
|
Reviewed-by: ppedrot
|
|
Ack-by: Blaisorblade
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
This should ideally have been done before the 8.11 branching.
|
|
Reviewed-by: ppedrot
|
|
- only one space instead of two when printing "{| |}"
- removing a redundant clause in the grammar of record_patterns
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
a module
Reviewed-by: ppedrot
|
|
|
|
|
|
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
|
|
|
|
|
|
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.
|
