| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
This is extracted from #9710, where we need the environment anyway to compute
iota rules on inductive types with let-bindings. The commit is self-contained,
so I think it could go directly in to save me a few rebases.
Furthermore, this is also related to #11707. Assuming we split cbn from the
other reduction machine, this allows to merge the "local" machine with
the general one, since after this PR they will have the same type. One less
reduction machine should make people happy.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
```
|
|
Matthieu Sozeau explained how to fix this.
|
|
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
|
|
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.
|
|
Some of them are significant so presumably it will take a bit of
effort to fix overlays.
I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
|
|
Reviewed-by: CohenCyril
Ack-by: Zimmi48
Ack-by: erikmd
Ack-by: gares
Ack-by: jfehrle
|
|
|
|
* "under"-specific behavior:
the order of goals is kept even if one issues
Global Set SsrOldRewriteGoalsOrder.
* href: https://github.com/math-comp/math-comp/blob/mathcomp-1.7.0/mathcomp/ssreflect/ssreflect.v
|
|
|
|
|
|
|
|
|
|
* If this flag under=true: enable flag with_evars of refine_with
to create evar(s) if the "under lemma" has non-inferable args.
* Backward compatibility of ssr rewrite is kept.
* Fix test-suite/ssr/dependent_type_err.v
|
|
|
|
|
|
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).
|
|
|
|
Deletes the SsrProfiling and SsrMatchingProfiling options
|
|
|
