| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
| |
This reverts commit 1d4c34c79624fb81e64dfed8874b2fc9fa66c070.
It seems the proof terminator of obligation.ml, in the case in which
Set Shrink Obligation is set, accesses the opaque proof.
|
| | |
|
| |
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |/ |
|
| | |
|
| | |
|
| |
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
|
| |
|
|
|
|
| |
allows for a simpler re-printing of assert.
Also fixing the precedence for printing "by" clause.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
variables" when matching over "{v : _ | _ & _}" which hides twice the
binding "fun v" since it is "sig2 (fun v => _) (fun v => _)".
Computing the bound variables statically at internalisation time
rather than every time at interpretation time. This cannot hurt even
if I don't know how to deal with the "notation" problem of a single
bound variable actually hiding two: at the current time, the notation
is printed only if the two variables are identical (see #4592), so,
with this semantics the warning should not be printed, but we lost the
information that we are coming from a notation; if #4592 were
addressed, then one of the binding should be alpha-renamed if they
differ, so collision should be solved by choosing the variable name
which is not renamed, but the matching algorithm should then be aware
of what the notation printing algorithm is doing... maybe not the most
critical thing at the current time.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
This type was actually only used by the debug printer of tactics, and only
for atomic tactics. Furthermore, that type was asymmetric, as the underlying
tacexpr type was set to be glob_tactic, when the semantics would have required
a Val.t type.
Furthermore, this type is absent from every contrib I have seen, which hints
again in favour of its lack of meaning.
|
| | |
|
| |\
| |
| |
| | |
into JasonGross-trunk-function_scope
|
| | |
| |
| |
| |
| |
| | |
It was only used by setoid_ring for the Add Ring command, and was easily
replaced by a dedicated argument. Moreover, it was of no use to tactic
notations.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
Enrico Tassi
Maxime Dénès
Emilio Jesus Gallego Arias
Matthieu Sozeau
Hugo Herbelin
Guillaume Melquiond
Pierre-Marie Pédrot
Daniel de Rauglaudre
Matej Kosik
Cyprien Mangin