| Commit message (Collapse) | Author | Age |
|\ |
|
| |
| |
| |
| | |
between proofs in tactic injection, with a side-effect on inversion.
|
|\| |
|
| |\
| | |
| | |
| | |
| | | |
Was PR#280: Document that [Reset Ltac Profile] is not synchronized with
the document state
|
| |\ \ |
|
| |\ \ \
| | | | |
| | | | |
| | | | | |
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.
|
| | | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
As noted by @ppedrot, the first is redundant. The patch is basically a renaming.
We didn't make the component optional yet, but this could happen in a
future patch.
|
|/ / / |
|
|\| | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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
|
| | | | |
|
| | | | |
|
| |/ /
|/| | |
|