| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: JasonGross
Ack-by: erikmd
Reviewed-by: maximedenes
Ack-by: proux01
|
|
Reviewed-by: gares
|
|
Previsouly, it was silently ignored.
|
|
|
|
|
|
projections
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
Async causes output reordering in one test. Since we don't care about
the output of that test (it's just a [Fail]) we move it to success/.
|
|
A scope delimiter was missing for primitive integers constants.
Add related regression tests.
|
|
Since e1e7888, stuck projections were not computed correctly.
Fixes #9684
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Ack-by: ppedrot
Ack-by: proux01
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: jfehrle
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
Ack-by: JasonGross
Reviewed-by: ppedrot
|
|
This removes various compatibility notations.
Closes #8374
This commit was mostly created by running `./dev/tools/update-compat.py
--release`. There's a bit of manual spacing adjustment around all of the
removed compatibility notations, and some test-suite updates were done
manually.
The update to CHANGES.md was manual.
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
RealField.v is slightly modified so that the ring/field tactics
consider the term (IZR (Z.pow_pos 10 _)) produced when parsing
exponents as constants.
|
|
Rather than integers '[0-9]+', numeral constant can now be parsed
according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'.
This can be used in one of the two following ways:
- using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin
- using `Numeral Notation` with the type `decimal` added to `Decimal.v`
See examples of each use case in the next two commits.
|
|
#9615)
Reviewed-by: Zimmi48
Ack-by: fajb
Reviewed-by: vbgl
|
|
|
|
- Improved reification for Micromega (support for #8764)
- Fixes #9268: Do not take universes into account in lia reification
Improve #9291 by threading the evar_map during reification.
Universes are unified.
- Remove (potentially cyclic) dependency over lra for Rle_abs
- Towards a complete simplex-based lia
fixes #9615
Lia is now exclusively using cutting plane proofs.
For this to always work, all the variables need to be positive.
Therefore, lia is pre-processing the goal for each variable x
it introduces the constraints x = y - z , y>=0 , z >= 0
for some fresh variable y and z.
For scalability, nia is currently NOT performing this pre-processing.
- Lia is using the FSet library
manual merge of commit #230899e87c51c12b2f21b6fedc414d099a1425e4
to work around a "leaked" hint breaking compatibility of eauto
|
|
Reviewed-by: ejgallego
Reviewed-by: jashug
|
|
This fixes #9767 by silently ignoring input lines which are not valid
UTF-8. We hereby assume that all file paths are valid UTF-8.
We also now actually test both python2 and python3 on the CI.
|
|
(warn if bar is a nonprimitive projection)
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: pi8027
|
|
Reviewed-by: Zimmi48
|
|
- test-suite/bugs/closed/xx.v renamed to .../bug_xx.v
- test-suite/failure/inductive4.v is now .../inductive.v
- repro for #4157 now added to the repo (it was in an unmerged commit
on @herbelin's repo)
- commit message of 244d7a9aa contains a repro for its bug (I didn't
bother adding to the test suite as a return of the bug could just as
well use different strings so the specific repro wouldn't test
anything useful)
|
|
Ack-by: ggonthier
Reviewed-by: mattam82
|
|
Ack-by: gares
Ack-by: maximedenes
|
|
In particular evar_eqappr_x tries to find a miller pattern on both sides,
while the fast path for evars tries solve_simple_eqn in one direction
only. So if you have (Evar-not-miller = Evar-miller) the code was not
trying to solve the RHS.
|
|
Previously, they were hard-wired in the ML code.
|
|
Eliminators can be:
- dependent: ... -> forall x (y : I x), P x y
- truncated: ... -> forall x (y : I x), P x
- funind like: ..-> forall x, P t
The user may provide a term t in `elim: t`
- t may be the last argument
- t may be the last "pattern" (standing for the last
argument of P)
We use unification to see if t (and its type) fits
in one of these cases (and/or to infer t).
This patch refuses to use unification in the HO case
eg `?T a = t` since the result is too often a false
positive.
|
|
|
|
proj
Ack-by: gares
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
applications
Reviewed-by: SkySkimmer
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: jfehrle
|
|
This fixes an incompleteness of subtyping on cumulative inductives,
where I@{i} A <= I@{j} A should imply i <= j, i = j or no relation
depending on the variance of I's universe.
|
|
The `Coercion` command did report many ambiguous paths when one declared
multiple inheritances. This change makes the `Coercion` command to do not
report them when
1. all the coercion in the potentially ambiguous paths respect the uniform
inheritance condition and
2. functional compositions of the potentially ambiguous paths are convertible to
each other.
The first condition is not explicitly checked but is used to make the checking
process of the second condition easy.
The key idea of this change:
Let us consider a sequence of coercion
f_1 : C_1 >-> C_2, f_2 : C_2 >-> C_3, ..., f_n : C_n >-> C_(n+1)
which respect the uniform inheritance condition and where the user-defined
classes C_i have m_i parameters respectively (i <= n).
The functional composition f_1 . ... . f_n can be expressed as follows:
(fun x_1 ... x_(m_1) y =>
f_n _ ... _ (* m_n times repetition of holes *)
(...
(f_2 _ ... _ (* m_2 times repetition of holes *)
(f_1 x_1 ... x_(m_1) y))...)),
and the contents of all the holes can be determined (inferred) without leaving
any existential variables in them thanks to the uniform inheritance condition.
Misc:
- A test case for this change: test-suite/output/relaxed_ambiguous_paths.v
- Turn the ambiguous paths messages into warnings to do output test.
|
|
|
|
(NB: this needs relevance mark fixing)
|
|
Prevent errors when under annotating binders.
|
|
|
|
For nonsquashed:
Either
- 0 constructors
- primitive record
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
|
|
Reviewed-by: gares
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Ack-by: ppedrot
|
|
record
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: jashug
|
|
This causes the makefile to break due to dependencies when it fails,
and it's not worth adding a whole mess of code to catch the failure
for these files.
|
