| Commit message (Collapse) | Author | Age |
... | |
| | | | |
|
| | |/
| | |
| | |
| | |
| | |
| | |
| | | |
The V82 compatibility layer of the proof engine was used by cc
(congruence closure) for the sole purpose of maintaining an
environment and a sigma. We inline the corresponding env and sigma in
the state of cc algorithm to get rid of the compatibility layer.
|
| |/
|/|
| |
| |
| |
| | |
- 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.
|
|\ \
| | |
| | |
| | | |
too long.
|
| | | |
|
| |/
| |
| |
| |
| |
| | |
Ssreflect was using a very complex function performing amongst other things
refolding to check that a term was an applied inductive type. It now relies
on a simple reduction followed by term matching.
|
|/ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |/
|/|
| |
| |
| |
| |
| | |
This feature has been asked many times by different people, and allows to
have options in a module that are performed when this module is imported.
This supersedes the well-numbered cursed PR #313.
|
|\ \ |
|
|\ \ \
| | | |
| | | |
| | | | |
wish #4129)
|
|\ \ \ \ |
|
| |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
| |/ / / / / /
|/| | | | | | |
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Attempt to extract the current ongoing proof (request by
Clément Pit-Claudel on coqdev, and also #4129).
Evars are handled as axioms.
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
This is a bit artificial since the extraction normally operates on
finished constrs (with no evars). But:
- Since we use Retyping quite a lot, switching to EConstr.t allows
to get rid of many `EConstr.Unsafe.to_constr (... (EConstr.of_constr ...))`
- This prepares the way for a possible extraction of the content
of ongoing proofs (a forthcoming `Show Extraction` command, see #4129 )
|
| | | | | | | |/ /
| | | | | | |/| |
| | | | | | | | |
| | | | | | | | | |
We replace constr by EConstr.t everywhere, and propagate some extra sigma args
|
| |_|/ / / / / /
|/| | | | | | | |
|
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
|
| |_|_|_|_|/ /
|/| | | | | | |
|
|\ \ \ \ \ \ \ |
|
| | | | | | | | |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \
| |_|_|_|_|/ / / /
|/| | | | | | | | |
|
| | | | | | | | | |
|
| |_|_|_|/ / / /
|/| | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
ocamldoc chokes on the markers {{{ and }}} because { and } are part of
its syntax
|
| |_|/ / / / /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This is needed in order to manipulate/serialize SSR's AST.
A quicker [and maybe better] alternative would be to just remove
`ssrparser.mli`, as there are many grammar entries that still need
exporting.
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ |
|
| |_|_|/ / / / /
|/| | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Following up on #6791, we remove:
- `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes`
- `Match Strict` a deprecated NOOP.
|
| | | | | | | | |
|
| |_|_|/ / / /
|/| | | | | | |
|
| | | | | | | |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Ssripats and Ssrview are now written in the Tactic Monad.
Ssripats implements the => tactical.
Ssrview implements the application of forward views.
The code is, according to my tests, 100% backward compatible.
The code is much more documented than before.
Moreover the "ist" (ltac context) used to interpret views is the correct
one (the one at ARGUMENT EXTEND interp time, not the one at TACTIC
EXTEND execution time). Some of the code not touched by this commit
still uses the incorrect ist, so its visibility in TACTIC EXTEND
can't be removed yet.
The main changes in the code are:
- intro patterns are implemented using a state machine (a goal comes
with a state). Ssrcommon.MakeState provides an easy way for a tactic
to enrich the goal with with data of interest, such as the set of
hyps to be cleared. This cleans up the old implementation that, in
order to thread the state, that to redefine a bunch of tclSTUFF
- the interpretation of (multiple) forward views uses the state to
accumulate intermediate results
- the bottom of Sscommon collects a bunch of utilities written in the
tactic monad. Most of them are the rewriting of already existing
utilities. When possible the old version was removed.
|
|\ \ \ \ \ \ \
| |/ / / / / /
|/| | | | | | |
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
coretactics.ml4.
|
|\ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|/ /
|/| | | | | | | | |
|