| Commit message (Collapse) | Author | Age |
|\
| |
| |
| | |
Was PR#232: Fix the parsing of goal selectors.
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | | |
as suggested by Hugo. Also, escape the spaces after the dots to obtain
a better PdfLaTeX output.
|
| | |
| | |
| | |
| | |
| | |
| | | |
- Ensure "coq_makefile --help" is properly typeset with HeVeA/PdfLaTeX
- Replace 's with "s so they are typeset as true ASCII characters
- Add missing ; before closing brace.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
~True.
Found 1 incompatibility in tested contribs and 3 times the same
pattern of incompatibility in the standard library. In all cases, it
is an improvement in the form of the script.
New behavior deactivated when version is <= 8.5.
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
(Fixed #4985)
Lqa.v defines the tactics lra and nra working over Q.
Lra.v defines the tactics lra and nra working over R.
|
| | | |
|
| | | |
|
| | | |
|
|\| | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Further work would include:
- Identify binders up to alpha-conversion (see #4932 with a list of
binders of length at least 2, or #4592 on printing notations such as
ex2).
A cool example that one could also consider supporting:
- Notation "[[ a , .. , b | .. | a , .. , b ]]" :=
(cons (cons a .. (cons b nil) ..) .. (cons a .. (cons b nil) ..) ..).
|
| | |
| | |
| | |
| | | |
We also add a Coq86.v compat file.
|
| | | |
|
| |/
|/| |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| | |
Unset Program Generalized Coercion to avoid coercion of general
applications.
Unset Program Cases to deactivate generation equalities and
disequalities of cases.
|
|\ \
| | |
| | |
| | | |
Was PR#207: Add -no-print-dependent-evars
|
| | | |
|
|\ \ \
| | |/
| |/| |
|
| | |
| | |
| | |
| | | |
Cf CHANGES for details.
|
| | |
| | |
| | |
| | | |
with recent Coq
|
| |/
|/|
| |
| |
| | |
This allows a work-around for bug #4819,
https://coq.inria.fr/bugs/show_bug.cgi?id=4819.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This commit documents par:, fixes its semantics so that is
behaves like all:, supports (toplevel) abstract and optimizes
toplevel solve.
`par: solve [tac]` is equivalent to `Ltac tac1 := solve[tac]...par: tac1`
but is optimized for failures: if one goal fails all are aborted
immediately.
`par: abstract tac` runs abstract on the generated proof terms. Nested
abstract calls are not supported.
|
| | |
|
| |
| |
| |
| |
| | |
As noticed by C. Cohen it was confusingly different from standard
notation.
|
|\ \ |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | | |
Documentation also updated.
|
|\ \ \
| |/ /
|/| |
| | | |
This is the "error resiliency" mode for STM
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This fixes the declarations of constraints, universes
and assumptions:
- global constraints can refer to global universes only,
- polymorphic universes, constraints and assumptions can only be
declared inside sections, when all the section's
variables/universes are polymorphic as well.
- monomorphic assumptions may only be declared in section contexts
which are not parameterized by polymorphic universes/assumptions.
Add fix for part 1 of bug #4816
|
| | | | |
|
| | | | |
|
| |/ /
|/| | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is suboptimal, because mutation leaves room for subtle bugs, but
rewriting @tebbi's code to be functional was a pain, and not something I
could figure out how to do easily. I'm working under the assumption
that there is no sharing in a single treenode, which I'm not completely
sure is valid. That said, a few simple tests seem to indicate that this
works as expected.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
https://github.com/coq/coq/pull/150#issuecomment-219141596
```bash
git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i
```
|
|/ / |
|
| | |
|
| | |
|
| | |
|
|\| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
preserved, which is a source of incompatibilities w.r.t. released 8.5
but which looks to me to be the only possible canonical behavior.
This is I believe a better behavior than the Regular Subst Tactic
behavior in the released 8.5 and 8.5pl1. There, the order of
hypotheses in which substitutions happened was respected, but their
interleaving with other hypotheses was not respected.
So, I consider this to be a fix to the "Regular Subst Tactic" mode.
Also added a more detailed "specification" of the "Regular" behavior
of "subst" in the reference manual.
|
|\| |
|
| | |
|