| Age | Commit message (Collapse) | Author |
|---|
|
location function
Reviewed-by: ppedrot
|
|
Ack-by: JasonGross
Reviewed-by: herbelin
Reviewed-by: jashug
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
We also get rid of ploc.ml, now useless, relying a priori on more
robust code in lStream.ml for location reporting (see
e.g. parse_parsable in grammar.ml).
|
|
Reviewed-by: mattam82
Ack-by: Zimmi48
|
|
instead of catching `Not_found`
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: vbgl
|
|
catching `Not_found`
`Global.lookup_constant` fails with an assertion instead of `Not_found`. Some
code relied upon `Not_found`.
|
|
- to zify the conclusion, we are using Tactics.apply (not rewrite)
Closes #11089
- constrain the arguments of Add Zify X to be GlobRef.t
Unset Primitive Projections so that projections are GlobRef.t.
Closes #14043
Update doc/sphinx/addendum/micromega.rst
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
The role of the `zify_saturate` tactic is to augment the goal with
positivity constraints. The premisses were previously obtained from
the context. If they are not present, we instantiate the saturation
lemma anyway.
Also,
- Remove saturation rules for Z.mul, the reasoning is performed by lia/nia
- Run zify_saturate after zify_to_euclidean_division_equations
- Better lemma for Z.power
- Ensure that lemma are generated once
Co-authored-by: Andrej Dudenhefner <mrhaandi>
Closes #12184, #11656
|
|
Reviewed-by: vbgl
|
|
The vernacular command takes a reference instead of a constr.
Moreover, the head symbol is checked i.e
Add Zify InjTyp ref checks that the referenced term has type
Intyp X1 ... Xn
Closes #14054, #13242
Co-authored-by: Vincent Laporte <vbgl@users.noreply.github.com>
|
|
|
|
Reviewed-by: Zimmi48
Ack-by: JasonGross
Ack-by: silene
Ack-by: SkySkimmer
Ack-by: olaure01
|
|
At first view, the fix takes care about when to use the number of
assumptions and when to also include local definitions, but I don't
know all the details of the implementation to be absolutely sure.
|
|
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
|
|
As of today Coq has the `CProfile` infrastructure disabled by default,
untested, and not easily accessible.
It was decided that `CProfile` should remain not user-accessible, and
only available thus by manual editing of Coq code to switch the flag
and manually instrument functions.
We thus remove all bitrotten dead code.
|
|
[structures]
Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
Reviewed-by: MSoegtropIMC
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Before you ask, the Ltac2.Ltac1 module is voluntarily underdocumented.
Fixes #13996: missing Ltac1.to_ident.
|
|
|
|
Reviewed-by: ppedrot
|
|
This tends to confuse the OCaml compiler, for good reasons. Indeed, if
there are mutable fields, the generated code cannot wait for the function
to be fully applied. It needs to recover the value of the mutable fields
as early as possible, and thus to create a closure.
Example:
let foo {bar} x = ...
is compiled as
let foo y = match y with {bar} -> fun x -> ...
|
|
|
|
As a bonus ltac2 can produce bullet suggestions.
|
|
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Instead of taking a type and checking that the inferred type for the expression
is correct, we simply pick an optional constraint and return the type directly
in the callback. This prevents having to compute type conversion twice in the
special case of Ltac2 variable quotations.
This should be 1:1 equivalent to the previous code, we are just moving code
around.
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
ssreflect asks setoid rewrite to rewrite in goal
"forall_special_name_ : T, _other_name_"
Since this is a non dependent product, setoid rewrite converts that to
"impl T _other_name_" and must be taught to restore the special name
when unfolding impl.
|
|
We introduce a new package structure for Coq:
- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`
This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.
The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.
Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.
There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.
This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.
IMHO the plan should work fine.
|
|
This was deprecated in 8.12
|
|
Signed primitive integers defined on top of the existing unsigned ones
with two's complement.
The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.
Additions to the kernel:
les (signed <=), lts (signed <), compares (signed compare),
divs (signed division), rems (signed remainder),
asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)
The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).
A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.
|
|
|
|
Closes #13794
|
|
Also added a generic way of temporarily disabling a warning.
Also added try_finalize un lib/utils.ml.
|
|
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
section/module closing time
Reviewed-by: SkySkimmer
|
|
|
|
Fixes #13755 .
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
The goal is to eventually only use the Simplex solver and
remove all the code needed for fourier elimination.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
Ack-by: Zimmi48
Ack-by: gares
Reviewed-by: ppedrot
|
