| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
-> "constr"
Reviewed-by: herbelin
Ack-by: Zimmi48
|
|
|
|
Fix #13045
Also make sure future anomalies won't be fed to tclzero.
Instead of retyping with lax:true we may question why we produce an
ill-typed term in decompose_app_rel: in the
| App (f, [|arg|]) ->
case we produce `fun x y : T => bla x y` but we have no assurance that
the second argument of `bla` should have type `T`.
|
|
|
|
Fix #12917
|
|
Reviewed-by: ppedrot
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: VincentSe
Ack-by: herbelin
Ack-by: olaure01
|
|
|
|
|
|
The doc states it is deprecated since 1386cd9 but this was ages before the
deprecation mechanism existed.
|
|
We finally pass the location in the "ist", and keep it in the "VFun"
which is associated to expanded Ltac constants.
|
|
|
|
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.
|
|
|
|
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.
|
|
|
|
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.
|
|
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.
|
|
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 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: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
|
|
It was deprecated in 8.12 and not used in the wild.
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Ack-by: gares
Ack-by: ppedrot
|
|
Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.
I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.
There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...
|
