| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Porting them is still to be done, but at least we don't rely on the wrapper
everywhere.
|
|
Add headers to a few files which were missing them.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
It was virtually unused except in ssr, and there is no reason to clutter
the kernel with irrelevant code.
Fixes #9390: What is the purpose of the function "kind_of_type"?
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
* Preserve the same behavior/interface but merge the two Module Types
(UNDER_EQ and) UNDER_REL.
* Remove the "Reflexive" argument in Under_rel.Under_rel
* Update plugin code (ssrfwd.ml) & Factor-out the main step
* Update the Hint (viz. apply over_rel_done => apply: over_rel_done)
* All the tests still pass!
Credits to @CohenCyril for suggesting this enhancement
|
|
try/with->assert false
as suggested by @gares (the Not_found exc may be catched by coq/ssr otherwise).
|
|
Changes:
* Add ssrclasses.v that redefines [Reflexive] and [iff_Reflexive];
* Add ssrsetoid.v that links
[ssrclasses.Reflexive] and [RelationClasses.Reflexive];
* Add [Require Coq.ssr.ssrsetoid] in Setoid.v;
* Update ssrfwd.ml accordingly, using a helper file ssrclasses.ml that
ports some non-exported material from rewrite.ml;
* Some upside in passing: ssrfwd.ml no more depends on Ltac_plugin;
* Update doc and tests as well.
Summary:
* We can now use the under tactic in two flavors:
- with the [eq] or [iff] relations: [Require Import ssreflect.]
- or a [RewriteRelation]: [Require Import ssreflect. Require Setoid.]
(while [ssreflect] does not require [RelationClasses] nor [Setoid],
and conversely [Setoid] does not require [ssreflect]).
* The file ssrsetoid.v could be skipped when porting under to stdlib2.
|
|
* Add an extra test with an Equivalence.
* Update the doc accordingly.
|
|
|
|
The current situation is a mess, some functions set it by default, but other
no. Making it mandatory ensures that the expected value is the correct one.
|
|
so it acts "more naturally" like (under eq_bigl; [hnf|]); move=> [*|].
Also: replace "by over." in the doc example with "over."
|
|
as suggested by @gares, and:
* Rename some Under_* terms for better uniformity;
* Update & Improve minor details in the documentation.
|
|
* Add tests accordingly.
|
|
|
|
In particular, this enhances support for lemma eq_big (with 2 side-conditions).
|
|
|
|
|
|
|
|
|
|
As a result, the following:
under i: eq_bigr by rewrite adnnC. (* ensure 1 Under subogal is created *)
under i: eq_big by [rewrite adnnC | rewrite addnC]. (* 2 Under subgoals *)
amounts to:
under i: eq_bigr; [rewrite adnnC; over | cbv beta iota].
under i: eq_big; [rewrite adnnC; over | rewrite adnnC; over | cbv beta iota].
|
|
in the particular case where the side-condition is phrased
(_ : @eqfun bool I P1 P2)
instead of
(_ : forall x : I, P1 x = P2 x)
|
|
Supported syntax:
under i: eq_bigr by rewrite adnnC. (* ensure 1 Under subogal is created *)
under i: eq_big by [rewrite adnnC | rewrite addnC]. (* 2 Under subgoals *)
Equivalent, expanded form:
under i: eq_bigr; [rewrite adnnC; over | idtac].
under i: eq_big; [rewrite adnnC; over | rewrite adnnC; over | idtac].
|
|
Rename the bound variables of the last (lambda) argument of the redex
w.r.t. the varnames specified by the user.
Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
|
|
Still to do: renaming the bound variables afterwards
|
|
|
|
This should make https://github.com/coq/coq/pull/9129 easier.
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
|
|
|
|
This commit implements the following intro patterns:
Temporary "=> +"
"move=> + stuff" ==== "move=> tmp stuff; move: tmp"
It preserves the original name.
"=>" can be chained to force generalization as in
"move=> + y + => x z"
Tactics as views "=> /ltac:(tactic)"
Supports notations, eg "Notation foo := ltac:(bla bla bla). .. => /foo".
Limited to views on the right of "=>", views that decorate a tactic
as move or case are not supported to be tactics.
Dependent "=> >H"
move=> >H ===== move=> ???? H, with enough ? to
name H the first non-dependent assumption (LHS of the first arrow).
TC isntances are skipped.
Block intro "=> [^ H] [^~ H]"
after "case" or "elim" or "elim/v" it introduces in one go
all new assumptions coming from the eliminations. The names are
picked from the inductive type declaration or the elimination principle
"v" in "elim/v" and are appended/prepended the seed "H"
The implementation makes crucial use of the goal_with_state feature of
the tactic monad. For example + schedules a generalization to be performed
at the end of the intro pattern and [^ .. ] reads the name seeds from
the state (that is filled in by case and elim).
|
|
|
|
The previous implementation was calling a lot of useless unification
even though the net effect of the tactic was simply to add a binding to
the environment.
Interestingly the base tactic was used in several higher level tactics,
including evar and ssreflect pose.
Part of the fix for #8245.
|
|
IIUC, this was a hack to make `Set SsrHave NoTCResolution` behave like
`Global Set SsrHave NoTCResolution`. I don't think it is needed (just
let the user write the desired locality), but if it is, the right way of
doing it is to let clients of Goptions specify a default locality.
|
|
|
|
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
|
Uses internal to Refiner remain.
|
|
|
|
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.
|
|
|
|
We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.
This is a step towards having a single module for `Constr`.
|
