| Age | Commit message (Collapse) | Author |
|---|
|
lambda
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
Opaque/Transparent
Reviewed-by: SkySkimmer
|
|
Reviewed-by: ppedrot
|
|
not an integer
Reviewed-by: ppedrot
|
|
|
|
(zero references is currently a no-op)
|
|
integer
|
|
|
|
Note: "hyp" was documented in Ltac Notation chapter but "var" was not.
|
|
deprecated.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: ejgallego
|
|
The current implementation of par: is still in the STM, but is optional.
If the STM does not take over it, it defaults to the implementation of
in comTactic which is based on all: (i.e. sequential).
This commit also moved the interpretation of a tactic from g_ltac to
vernac/comTactic which is more appropriate.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
An h-box inhibits the breaking semantics of any cut/spc/brk in the
enclosed box.
We tentatively replace its occurrence by an h or hv, assuming in
particular that if the indentation is not 0, an hv box was intended.
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
-> "constr"
Reviewed-by: herbelin
Ack-by: Zimmi48
|
|
|
|
Fix #13129
|
|
Remove unused arguments and commented code
|
|
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.
|
