| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |\ \ \ \ \ \ |
|
| | |_|_|_|_|/
|/| | | | |
| | | | | |
| | | | | | |
Following up on #6791, we remove the option "Intuition Iff Unfolding"
|
| | |_|_|/ /
|/| | | |
| | | | |
| | | | | |
Fix new deprecation warnings in the standard library.
|
| | |/ / /
|/| | | |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |\ \ \
| | | |
| | | |
| | | | |
Ring_theory.v)
|
| | |_|/
|/| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This allows in particular to define notations with 'pat style binders.
E.g.:
A non-trivial change in this commit is storing binders and patterns
separately from terms.
This is not strictly necessary but has some advantages.
However, it is relatively common to have binders also used as terms,
or binders parsed as terms. Thus, it is already relatively common to
embed binders into terms (see e.g. notation for ETA in output test
Notations3.v) or to coerce terms to idents (see e.g. the notation for
{x|P} where x is parsed as a constr).
So, it is as simple to always store idents (and eventually patterns)
as terms.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
For instance, the following is now possible:
Check {(x,y)|x+y=0}.
Some questions remains. Maybe, by consistency, the notation should be
"{'(x,y)|x+y=0}"...
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |/ / |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
camlp4
|
| |\ \ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
longer use camlp4.
|
| | |_|/ / /
|/| | | | |
|
| | |_|_|/
|/| | |
| | | |
| | | |
| | | | |
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).
|
| |\ \ \ |
|
| |\ \ \ \
| |_|/ /
|/| | | |
|
| | | | | |
|
Maxime Dénès
Emilio Jesus Gallego Arias
Enrico Tassi
Théo Zimmermann
Hugo Herbelin
Jim Fehrle
Joachim Breitner
Gaëtan Gilbert
Vincent Laporte
Paul Steckler
Jasper Hugunin