| Age | Commit message (Collapse) | Author |
|---|
|
|
|
In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in
1.10, see
https://github.com/ocaml/Zarith/issues/58
|
|
We still link num in `coqc` , that will be removed in a separate step.
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: pi8027
Reviewed-by: ppedrot
|
|
|
|
This is necessary to support OCaml 4.11 in development.
|
|
Keep Numeral Notation wit a deprecation warning.
|
|
|
|
Negative values had no meaning there.
Those were spotted by Hugo Herbelin while reviewing #12979 .
|
|
|
|
|
|
Reviewed-by: cpitclaudel
Reviewed-by: ppedrot
|
|
|
|
vice versa
|
|
|
|
This is a follow-up of #9062, which introduced a discrenpancy between
the two unification engines.
|
|
Reviewed-by: SkySkimmer
Ack-by: herbelin
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
Ack-by: SkySkimmer
|
|
of ZArith.
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: liyishuai
Ack-by: MSoegtropIMC
Ack-by: ejgallego
Ack-by: maximedenes
Ack-by: proux01
Ack-by: vbgl
|
|
renaming.
Example:
> Arguments id [B] {b} : rename.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Argument B is a trailing implicit, so it can't be declared non
maximal. Please use { } instead of [ ].
|
|
|
|
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml
library which is a more modern version.
We switch the core files and easy plugins only for now, more complex
numerical plugins will be done in their own commit.
We thus keep the num library linked for now until all plugins are
ported.
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
|
|
|
|
This makes the test suite Omega.v compatible with Mangle Names
Not sure how `reintroduce` works since it ignores the refreshed name,
considering omega is deprecated it's not worth figuring out so long as
it works (NB making it use intro_mustbe_force makes the test suite
fail so it must be doing something right).
|
|
|
|
Fix #12889
|
|
declaring name
Reviewed-by: maximedenes
|
|
Reviewed-by: ppedrot
|
|
Amends c1b1afe76e1655cc3275bdf4215f0ab690efc3cc
|
|
When calling an Ltac function, add specific locations when
interpreting the function, when interpreting the arguments and when
executating the call (in a TacArg).
|
|
This is important for TacArg arguments, which typically corresponds to
calling an Ltac function.
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
If we need to print the name of an inlined constant (as in "let name =",
"val name :" or "type name ="), we need its name without inlining nor
qualification.
In particular, we introduce a function pp_global_name to make it
clearer that printing a name at declaration point of a global is only
about printing the basename (formerly, Common.pp_global was correctly
printing the basename without qualification thanks to the
"top_visible_mp ()" test, but OCaml.pp_global was wrongly inlining).
|
|
The update of a loc needs sometimes to override (when calling an Ltac
function), and otherwise to keep the existing loc (assumed to be
fined). We refine this (see e.g. the ErrorLocation_tac_in_term tests).
Moreover, when overriding, this was going to a tclOR backtracking
point which was setting the loc to a completely disjoint part of the
code having caused the error (see #12773). We replace the tclOR by a
tclORELSE.
|
|
Reviewed-by: vbgl
|
|
Reviewed-by: vbgl
|
|
zify used to generate many syntactic positivity constraints when translating a goal
from nat to Z. For instance, to state that the product of 2 integers
is positive. Instead, lia performs an interval analysis that is more semantic.
The bug was that the interval analysis was performed after the
elimination of equations. The current workaround is to perform
interval analysis before and after eliminating equations.
bla
|
|
The elimination of let bindings is performing a convertibility check in
order to deal with type aliases.
|
|
|
|
|
|
of standard infrastructure.
Reviewed-by: ppedrot
|
|
Apart from being verboten to marshal Environ.env, this should use much less
memory on-disk.
Fixes #12707.
|
|
infrastructure.
The old wrapper was basically unused, this PR also fixes backtraces in
some class of bugs such as https://github.com/coq/coq/issues/12695
|
|
|
|
In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.
Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.
We make this manipulation explicit by handling the program state
functionally, in a similar way than we already do for lemmas.
This requires to extend the proof DSL a bit; but IMO changes are
acceptable given the gain.
Most of the PR is routine; only remarkable change is that the hook is
called explicitly in `finish_admitted` as it had to learn about the
different types of proof_endings.
Note that we could have gone deeper and use the type system to refine
the core proof type; IMO it is still too preliminary so it is better
to do this step as an intermediate one towards a deeper unification.
|
|
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
