| Age | Commit message (Collapse) | Author |
|---|
|
by doing the same thing as `zify_nat` does for `nat.pred`.
This fixes #6602.
|
|
In current code, `Proofview.Goal.t` uses a phantom type to indicate
whether the goal was properly substituted wrt current `evar_map` or
not.
After the introduction of `EConstr`, this distinction should have
become unnecessary, thus we remove the phantom parameter from
`'a Proofview.Goal.t`. This may introduce some minor incompatibilities
at the typing level. Code-wise, things should remain the same.
We thus deprecate `assume`. In a next commit, we will remove
normalization as much as possible from the code.
|
|
|
|
|
|
VernacDefinition
|
|
|
|
|
|
|
|
There is no way today to distinguish primitive projections from
compatibility constants, at least in the case of a record without
parameters.
We remedy to this by always using the r.(p) syntax when printing
primitive projections, even with Set Printing All.
The input syntax r.(p) is still elaborated to GApp, so that we can preserve
the compatibility layer. Hopefully we can make up a plan to get rid of that
layer, but it will require fixing a few problems.
|
|
|
|
|
|
Fixes #6490.
`prod_applist_assum` is copied from `kernel/term.ml` to `engine/termops.ml`,
and adjusted to work with econstr.
This change uncovered a bug in `Hipattern.match_with_nodep_ind`, where
`has_nodep_prod_after` counts both products and let-ins, but was only
being passed `mib.mind_nparams`, which does not count let-ins.
Replaced with (Context.Rel.length mib.mind_params_ctxt).
|
|
|
|
|
|
|
|
|
|
.dir-locals led to issues with unsafe local variable warnings. With
this method the user is opting in to running this code so there are no warnings.
|
|
This allows to focus on a sub-goal other than the first one without
resorting to the `Focus` command.
|
|
|
|
|
|
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
|
Some code in typeclasses was even breaking the invariant that
use_polymorphic_flag should not be called twice, but that code was
morally dead it seems, so we remove it.
|
|
|
|
|
|
Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.
In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.
|
|
It was the identity.
|
|
Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.
Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.
This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.
|
|
|
|
|
|
|
|
|
|
Extraction Language command
|
|
|
|
|
|
|
|
This is useful as it allows to reflect program_mode behavior as an attribute.
|
|
Over the time, `Command` grew organically and it has become now one of
the most complex files in the codebase; however, its functionality is
well separated into 4 key components that have little to do with each
other.
We thus split the file, and also document the interfaces. Some parts
of `Command` export tricky internals to use by other plugins, and it
is common that plugin writers tend to get confused, so we are more
explicit about these parts now.
This patch depends on #6413.
|
|
|
|
We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step
desirable to progress with EConstr there.
|
|
As per request at https://github.com/coq/coq/pull/6406#pullrequestreview-83503902
|
|
This closes #5082 and closes #5778, but makes #6404 apply to `abstract`
as well as `transparent_abstract`. This is unfortunate, but I think it
is worth it to get `abstract` in the profile (and therefore not
misassign the time spent sending the subproof to the kernel). Another
alternative would have been to add a dedicated entry to `ltac_call_kind`
for `TacAbstract`, but I think it's better to just deal with #6404 all
at once.
The "better" solution here would have been to move `abstract` out of the
Ltac syntax tree and define it via `TACTIC EXTEND` like
`transparent_abstract`. However, the STM relies on its ability to
recognize `abstract` and `solve [ abstract ... ]` syntactically so that
it can handle `par: abstract`.
Note that had to add locations to `TacAbstract` nodes, as I could not
figure out how to call `push_trace` otherwise.
|
|
|
|
|
|
I'm not sure if they belong in profile_ltac, or in extratactics, or,
perhaps, in a separate plugin. But I'd find it very useful to have a
version of `time` that works on constr evaluation, which is what this
commit provides.
I'm not sure that I've picked good naming conventions for the tactics,
either.
|
|
This is useful for tactics that run a bunch of tests and need to display
the profile for each of them.
|
|
|
|
(fix #6106)
|
|
|
|
same right-hand side.
|
|
|
