| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
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.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
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.
|
Pierre-Marie Pédrot
Matej Kosik
Maxime Dénès
Hugo Herbelin
Guillaume Melquiond
Enrico Tassi
Matthieu Sozeau
Daniel de Rauglaudre
Matej Kosik
Cyprien Mangin