| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
We use a lower level function that accesses the proof without raising an
anomaly. This is a direct candidate for backport, so I used a V82 API but
eventually this API should be cleaned up.
|
| |
|
|
|
|
| |
- The case 0 makes the code of intros until (and in particular of
Detyping.lookup_quantified_hypothesis_as_displayed more complicated).
- The introduction pattern "*" is compositional while "until 0" is not.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Tactic-in-term can be called from within a tactic itself. We have to
preserve the preexisting future_goals (if called from pretyping) and
we have to inform of the existence of pending goals, using
future_goals which is the only way to tell it in the absence of being
part of an encapsulating proofview.
This fixes #6313.
Conversely, future goals, created by pretyping, can call ltac:(giveup) or
ltac:(shelve), and this has to be remembered. So, we do it.
|
| | |
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ |
|
| | |_|_|/ / / /
|/| | | | | | |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
|
| | |_|_|_|_|/
|/| | | | | |
|
| | |_|/ / /
|/| | | |
| | | | |
| | | | | |
Following up on #6791, we the option "Discriminate Introduction".
|
| | |/ / /
|/| | |
| | | |
| | | | |
Following up on #6791, we the option "Shrink Abstract".
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | |_|/ / /
|/| | | | |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| | |_|_|/ / /
|/| | | | | |
|
| | | | | | | |
|
| |\ \ \ \ \ \
| |/ / / / /
|/| | | | | |
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
coretactics.ml4.
|
| |\ \ \ \ \ \ \ \ |
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Following up on #6791, we remove the option "Standard Proposition Elimination"
|
| | | | | | | | |/
| | | | | | |/|
| | | | | | | |
| | | | | | | | |
Following up on #6791, we remove the option "Injection L2R Pattern Order".
|
| | | | | | |/ /
| | | | |/| | |
|
| | |_|_|/ / /
|/| | | | |
| | | | | |
| | | | | | |
Noticed by Sigurd Schneider.
|
| | |/ / / /
|/| | | | |
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| |/ / |
|
| |\ \ |
|
| | | | |
|
| | |/
|/| |
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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).
|
| | |
| |
| |
| |
| |
| |
| | |
We simply use a record and pack the rel and var substitutions in it. We also
properly compose variable substitutions.
Fixes #6534: Fresh variable generation in case of clash is buggy.
|
Pierre-Marie Pédrot
Hugo Herbelin
Emilio Jesus Gallego Arias
Gaëtan Gilbert
Maxime Dénès
Théo Zimmermann
mrmr1993
Enrico Tassi
Jasper Hugunin