| Age | Commit message (Collapse) | Author |
|---|
|
To prevent confusion, forbidding a mix of the "injection term as pat1
... patn" and of the "injection term as [= pat1 ... patn]" syntax: If
a "[= ...]" occurs, this should be a singleton list of patterns.
|
|
|
|
Typeclasses resolution is not used anymore for lia.
Typeclasses resolution is still used by lra but only to access a
database of declared constants.
|
|
Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: jashug
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: maximedenes
|
|
Reviewed-by: MSoegtropIMC
Ack-by: Zimmi48
Reviewed-by: amahboubi
Reviewed-by: vbgl
|
|
Incidentally, this fixes #10056
|
|
|
|
|
|
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: CohenCyril
Ack-by: Zimmi48
Ack-by: erikmd
Ack-by: gares
Ack-by: jfehrle
|
|
|
|
|
|
|
|
So if the underlying tactic "contains a ;" one should actually write:
under eq_bigl => i do [rewrite andb_idl; first by move/eqP->].
|
|
as suggested by @gares, and:
* Rename some Under_* terms for better uniformity;
* Update & Improve minor details in the documentation.
|
|
|
|
Ack-by: JasonGross
Ack-by: erikmd
Reviewed-by: maximedenes
Ack-by: proux01
|
|
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.
|
|
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
|
|
(warn if bar is a nonprimitive projection)
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: pi8027
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: jfehrle
|
|
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.
|
|
For nonsquashed:
Either
- 0 constructors
- primitive record
|
|
|
|
|
|
This is intended to be separate from handling of implicit binders.
The remaining uses of declare_manual_implicits satisfy a lot of
assertions, giving the possibility of simplifying the interface in the
future.
Two disabled warnings are added for things that currently pass silently.
Currently only Mtac passes non-maximal implicits to
declare_manual_implicits with the force-usage flag set. When implicit
arguments don't have to be named, should move Mtac over to
set_implicits.
|
|
Parameters had to be removed in cases_pattern_of_glob_constr.
|
|
Ack-by: Zimmi48
Reviewed-by: jfehrle
Ack-by: ppedrot
|
|
I think the usage looks cleaner this way.
|
|
This is only used for debugging, if a user wants more feedback she can turn
on the option. Conversely, it has a cost for any tactic script, so it is
wiser to disable it by default.
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
This PR deprecates the use of `coqtop` as a compiler.
There is no point on having two binaries with the same purpose; after
the experiment in #8690, IMHO we have a lot to gain in terms of code
organization by splitting the compiler and the interactive binary.
We adapt the documentation and adapt the test-suite.
Note that we don't make `coqc` a true binary yet, but here we take
care only of the user-facing part.
The conversion of the binary will take place in #8690 and will bring
code simplification, including a unified handling of arguments.
|
|
|
|
[About] still says it.
Close #9056.
|
|
This is a reworking of 7fd28dc9: instead of using words such as
"domain of", "codomain of" to refer to a position in the instance of
the original evar, we simply display the instance and the name of the
unresolved evar in this instance. This is both simpler and more
informative. (The positional words remain useful for printing the
evar_map in debugging though.)
In passing, this fixes #8369 (Not_found in printing message about an
unresolved subevar).
Incidentally add possible breaking while printing "in environment".
|
|
Thanks to Georges Gonthier for noticing it.
Expanding a few Pervasives.compare at this occasion.
|
|
|
|
|
|
You can tell which it is from the `@{}` if you really care, and seeing
`Monomorphic List (A:Type)` with no indication that `Monomorphic` is
about universes can confuse people.
|
|
The checks were unnecessarily restrictive (since names can be used for
documentation purposes), and the error message was a bit wrong (it
mentioned a restriction on the explicit status of arguments).
|
|
|
|
|
