| Commit message (Collapse) | Author | Age |
|\ |
|
| |
| |
| |
| |
| |
| |
| | |
- Adding a better location in the "apply" on the fly pattern.
- Printing statement of lemma and of hypothesis.
Was suggested by discussion at wish report #5390.
|
|\| |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| | |
named in the original term.
Useful at least for debugging, useful to give a better message than
"this placeholder", even if in the loc is known in this case.
|
|/| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing
changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341.
It turns out that calling from fake_ide the STM commands that were removed
by this PR requires an extension of the XML protocol. So postponing the
integration.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
I think these commands never make a lot of sense on scripts other than
debugging and we have better methods now.
The last remaining command, used for the tty emulation has been renamed
to VtBack, but it should go away at some point too once the legacy
interfaces are removed.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
|
|\| |
|
| |
| |
| |
| | |
generates garbage. So the comment is kept but it is not passed over to ocamldoc.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The main point of this change is to fix #3035: Avoiding trailing
arguments in the Arguments command, and related issues occurring in
HoTT for instance. When the "assert" flag is not specified, we now
accept prefixes of the list of arguments.
The semantics of _ w.r.t. to renaming has changed. Previously, it meant
"restore the original name inferred from the type". Now it means "don't
change the current name".
The syntax of arguments is now restricted. Modifiers like /, ! and
scopes are allowed only in the first arguments list.
We also add *a lot* of missing checks on input values and fix various
bugs.
Note that this code is still way too complex for what it does, due to
the complexity of the implicit arguments, reduction behaviors and renaming
APIs.
|
|\| |
|
| |
| |
| |
| | |
Also getting rid of a global side-effect.
|
|\ \ |
|
| |/
| |
| |
| |
| |
| |
| |
| |
| |
| | |
For now, the only meaningful user is "Set Warnings". Example:
Section Bar.
Local Set Warnings Append "-foo".
(* warning foo is now disabled *)
End Bar.
(* foo is now reenabled, assuming it was before entering the section *)
|
| |\
| | |
| | |
| | |
| | | |
Was PR#299: Fix bug #4869, allow Prop, Set, and level names in
constraints.
|
| | |
| | |
| | |
| | |
| | |
| | | |
This is a quick fix. The Metasyntax module should be thoroughly revised
in trunk, because it starts featuring a lot of spaghetti code and redundant
data.
|
| | |
| | |
| | |
| | |
| | | |
It seems warnings are not taken into account in output/
tests.
|
| |/ |
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
I hadn't realized that this PR uses OCaml's 4.03 inlined records
feature. I will advocate again for a switch to the latest OCaml stable
version, but meanwhile, let's revert. Sorry for the noise.
This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing
changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The new name makes it more obvious what is meant here by "kind". We leave
Decl_kinds.binding_kind as a deprecated alias for plugin
compatibility.
We also replace bool with implicit_status in a few places in the
codebase.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We get rid of tuples containing booleans (typically for universe
polymorphism) by replacing them with records.
The previously common idom:
if pi2 kind (* polymorphic *) then ... else ...
becomes:
if kind.polymorphic then ... else ...
To make the construction and destruction of these records lightweight,
the labels of boolean arguments for universe polymorphism are now
usually also called "polymorphic".
|
| | |
|
| | |
|
| | |
|
|/ |
|
| |
|
| |
|
|
|
|
| |
Cf CHANGES for details.
|
| |
|
|
|
|
|
| |
simplifying and generalizing the grammar entries for injection,
discriminate and simplify_eq.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
In pat%constr, creating new evars is now allowed only if "eintros" is
given, i.e. "intros" checks that no evars are created, and similarly
e.g. for "injection ... as ... pat%constr".
The form "eintros [...]" or "eintros ->" with the case analysis or
rewrite creating evars is now also supported.
This is not a commitment to say that it is good to have an e- modifier
to tactics. It is just to be consistent with the existing convention.
It seems to me that the "no e-" variants are good for beginners. However,
expert might prefer to use the e-variants by default. Opinions from
teachers and users would be useful.
To be possibly done: do that [= ...] work on hypotheses with side
conditions or parameters based on the idea that they apply the full
injection and not only the restriction of it to goals which are
exactly an equality, as it is today.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
| |
Suggested by R. Krebbers and C. Cohen, this makes modes
more applicable, by allowing to trigger resolution on partially
instantiated indices. This is a rough but fast approximation of the
pattern on which one would like instances to apply.
|
|
|
|
|
|
| |
simpler re-printing of assert.
Also fixing the precedence for printing "by" clause.
|
|\ |
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This allows to write things like this:
split; 2: intro _; exact I
or like this:
eexists ?[x]; ?[x]: exact 0; trivial
This has the side-effect on making the '?' before '[x]' mandatory.
|
| | |
| | |
| | |
| | |
| | | |
You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals
numbered 1 and 3 to 5.
|
| | | |
|
| |/ |
|
|/
|
|
|
|
|
|
|
|
|
|
| |
This commit introduces the concept of proof blocks that are
resilient to errors. They are represented as ErrorBound boxes
in the STM document with the topological invariant that they never
overlap.
The detection and error recovery of ErrorBound boxes is defined outside
the STM. One can define a box by providing a function to detect it
statically by crawling the parsed document and a function to recover
from an error at run time.
|
| |
|
| |
|
|
|
|
|
|
| |
Note that this breaks the compatibility, in a beneficial way I believe. Tactics
defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction
on a local identifier anymore. They must use the "fresh" primitive instead.
|
| |
|
|
|
|
| |
and Evar in notations, and there are anyway already forbidden.
|
| |
|