| Age | Commit message (Collapse) | Author |
|---|
|
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).
|
|
|
|
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>
|
|
|
|
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
|
|
After #12504 , we can encapsulate and consolidate low-level state
logic in `Vernacstate`, removing `States` which is now a stub.
There is hope to clean up some stuff regarding the handling of
low-level proof state, by moving both `Evarutil.meta_counter` and
`Evd.evar_counter_summary` into the proof state itself [obligations
state is taken care in #11836] , but this will take some time.
|
|
|
|
|
|
|
|
|
|
|
|
This is needed in rewriter as to avoid hack; indeed it makes sense to
propagate this information to the callers of save.
|
|
This completes the refactoring [for now] of the core `Declare`
interface, and will allow much internal refactoring in the future.
In particular, we remove the low-level Proof_ending type, and instead
introduce higher-level constructors for the several declare users.
Future PRs will change the internal representation of proof handling
to better enforce some invariants that should hold for specific
proofs.
|
|
This allows us to remove a large chunk of the internal API, and is the
pre-requisite to get rid of [Proof_ending], and even more refactoring
on the declare path.
|
|
We unify information about constants so it is shared among all the
paths [interactive, NI, obligations].
IMHO the current setup looks pretty good, with information split into
a per-constant record `CInfo.t` and variables affecting mutual
definitions at once, which live in `Info.t`.
Main information outside our `Info` record is `opaque`, which is
provided at different moments in several cases.
There are a few nits regarding interactive proofs, which will go away
in the next commits.
|
|
This is in preparation for the next commit which will clean-up the
current API flow in `Declare`.
|
|
|
|
|
|
This improves the interface, and allows even more sealing of the API.
This is yet work in progress.
|
|
The module is now a stub. We choose to be explicit on the parameters
for now, this will improve in next commits with the refactoring of
proof / constant information.
|
|
At this point the record in lemmas was just a stub; next commit will
stop exposing the internals of mutual information, and pave the way
for the refactoring of `Info.t` handling in the Declare interface.
|
|
Having two different modules led to the availability of internal API in
the mli.
|
|
|
|
|
|
Reviewed-by: CohenCyril
Reviewed-by: ppedrot
|
|
|
|
|
|
Add Zify <X> are documented.
Add <X> is deprecated as it clashed with the standard Add command
|
|
|
