| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
| |
We add a [SelectAlreadyFocused] constructor to [goal_selector] (read
"!") which causes a failure when there's not exactly 1 goal and
otherwise is a noop.
Then [Set Default Goal Selector "!".] puts us in "strict focusing"
mode where we can only run tactics if we have only one goal or use a
selector.
Closes #6689.
|
| |\ |
|
| | | |
|
| |/
|
|
|
|
| |
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
|
| |\
| |
| |
| | |
failure in other file
|
| |\ \ |
|
| | | | |
|
| | |/
|/| |
|
| |/
|
|
|
|
|
|
|
|
|
|
| |
We solve some modularity and type duplication problems by moving types
to a better place. In particular:
- We move tactics types from `Misctypes` to `Tactics` as this is their
proper module an single user [with LTAC].
- We deprecate aliases in `Tacexpr` to such tactic types.
cc: #6512
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Unfortunately, mli-only files cannot be included in packs, so we have
the weird situation that the scope for `Tacexpr` is wrong. So we
cannot address the module as `Ltac_plugin.Tacexpr` but it lives in the
global namespace instead.
This creates problem when using other modular build/packing strategies
[such as #6857] This could be indeed considered a bug in the OCaml
compiler.
In order to remedy this situation we face two choices:
- leave the module out of the pack (!)
- create an implementation for the module
I chose the second solution as it seems to me like the most sensible
choice.
cc: #6512.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
The `reference` type contains some ad-hoc locations in its
constructors, but there is no reason not to handle them with the
standard attribute container provided by `CAst.t`.
An orthogonal topic to this commit is whether the `reference` type
should contain a location or not at all.
It seems that many places would become a bit clearer by splitting
`reference` into non-located `reference` and `lreference`, however
some other places become messier so we maintain the current status-quo
for now.
|
| |
|
|
|
|
|
|
|
|
|
| |
We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:
- module declarations
- intro patterns
- top-level sentences
Now, parsed documents should be full annotated by `CAst` nodes.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative
inductive would try to generate a constraint [i = j] and use
cumulativity only if this resulted in an inconsistency. This is
confusingly different from the behaviour with [Type] and means
cumulativity can only be used to lift between universes related by
strict inequalities. (This isn't a kernel restriction so there might
be some workaround to send the kernel the right constraints, but
not in a nice way.)
See modified test for more details of what is now possible.
Technical notes:
When universe constraints were inferred by comparing the shape of
terms without reduction, cumulativity was not used and so too-strict
equality constraints were generated. Then in order to use cumulativity
we had to make this comparison fail to fall back to full conversion.
When unifiying 2 instances of a cumulative inductive type, if there
are any Irrelevant universes we try to unify them if they are
flexible.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic
and its parsing rule. Instead, we make it generate a typed AST that is
passed to the parser and a generic tactic execution routine.
PMP has written a small parser that can generate the same typed ASTs
without relying on camlp5, which is overkill for such simple macros.
|
| |/
|
|
| |
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
coretactics.ml4.
|
| |\ \ \ \ \ |
|
| | |_|_|_|/
|/| | | |
| | | | |
| | | | | |
Following up on #6791, we remove the option "Intuition Iff Unfolding"
|
| | |/ / /
|/| | | |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This commit was motivated by true spurious conversions arising in my
`to_constr` debug branch.
The changes here need careful review as the tradeoffs are subtle and
still a lot of clean up remains to be done in `vernac/*`.
We have opted for penalize [minimally] the few users coming from true
`Constr`-land, but I am sure we can tweak code in a much better way.
In particular, it is not clear if internalization should take an
`evar_map` even in the cases where it is not triggered, see the
changes under `plugins` for a good example.
Also, the new return type of `Pretyping.understand` should undergo
careful review.
We don't touch `Impargs` as it is not clear how to proceed, however,
the current type of `compute_implicits_gen` looks very suspicious as
it is called often with free evars.
Some TODOs are:
- impargs was calling whd_all, the Econstr equivalent can be either
+ Reductionops.whd_all [which does refolding and no sharing]
+ Reductionops.clos_whd_flags with all as a flag.
|
| | |/
|/| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.
With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.
|
| | | |
|
| | |
| |
| |
| | |
Renaming it register_grammars_by_name.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The motivations are:
- To reflect the concrete syntax more closely.
- To factorize the different places where "contexts" are internalized:
before this patch, there is a different treatment of `Definition f
'(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack
to interpret `Definition f `pat := c : t`. With the patch, the fix
to avoid seeing a variable named `pat` works for both `fun 'x =>
...` and `Definition f 'x := ...`.
The drawbacks are:
- Counterpart to reflecting the concrete syntax more closerly, there
are more redundancies in the syntax. For instance, the case `CLetIn
(na,b,t,c)` can appears also in the form `CProdN (CLocalDef
(na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`.
- Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.
|
| |
|
|
| |
longer use camlp4.
|
| | |
|
| |\ |
|
| |\ \ |
|
| | |/
|/|
| |
| |
| | |
This allows to focus on a sub-goal other than the first one without
resorting to the `Focus` command.
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
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.
|
| |/
|
|
| |
It was the identity.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
This is useful as it allows to reflect program_mode behavior as an attribute.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
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.
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
Gaëtan Gilbert
Pierre-Marie Pédrot
Hugo Herbelin
Jason Gross
Emilio Jesus Gallego Arias
Maxime Dénès
Théo Zimmermann
Enrico Tassi
Jim Fehrle
Paul Steckler