| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
notations in patterns than in terms, wrt implicit arguments and
scopes.
See file Notations2.v for the conventions in use in terms.
Somehow this could be put in 8.5 since it puts in agreement the
interpretation of abbreviations and notations in "symmetric patterns"
to what is done in terms (even though the interpretation rules for
terms are a bit ad hoc).
There is one exception: in terms, "(foo args) args'" deactivates the
implicit arguments and scopes in args'. This is a bit complicated to
implement in patterns so the syntax is not supported (and anyway, this
convention is a bit questionable).
|
|
|
|
|
|
|
|
This was redundant with the wit_uconstr generic argument, so there was no real
point on keeping it there.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- Making a clear distinction between expressions of the notation which
are associated to binding variables only (as in `Notation "'lam' x ,
P" := (fun x => P)" or `Notation "'exists2' x : t , p & q" := (ex2
(fun x:t => p) (fun x:t => q))') and those which are associated to
at list one subterm (e.g. `Notation "x .+1" := (S x)' but also
"Notation "{# x | P }" := (ex2 _ (fun y => x = F y) (fun x => P))'
as in #4592). The former have type NtnTypeOnlyBinder.
- Thus avoiding in particular encoding too early Anonymous as GHole
and "Name id" as "GVar id".
There is a non-trivial alpha-conversion work to do to get #4592
working. See comments in Notation_ops.add_env.
|
|
This was historically used together with the <:tactic< ... >> quotation to insert
foreign code as $foo, but it actually only survived in the implementation of Tauto.
With the removal of the quotation feature, this is now totally obsolete.
|
|
|
|
Fixpoint/Definition.
|
|
- Fixing dead code, doc.
- Relaxing constraints on using an as-tuple in inversion.
|
|
|
|
The length of the pattern should now be exactly the number of
assumptions and definitions introduced by the destruction or induction,
including the induction hypotheses in case of an induction.
Like for pattern-matching, the local definitions in the argument of
the constructor can be skipped in which case a name is automatically
created for these.
|
|
|
|
|
|
|
