| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
I have removed the second field of the "Constrexpr.CRecord" variant
because once it was set to "None"
it never changed to anything else.
It was just carried and copied around.
|
| | |
| |
| |
| | |
Actually the identifier was never used and just carried along.
|
| | |
| |
| |
| |
| | |
The TacAlias node now only contains the arguments fed to the tactic notation.
The binding variables are worn by the tactic representation in Tacenv.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This commit has deep consequences in term of tactic evaluation,
as it allows to pass any tac_arg to ML and alias tactics rather than
mere generic arguments. This makes the evaluation much more uniform,
and in particular it removes the special evaluation function for notations.
This last point may break some notations out there unluckily.
I had to treat in an ad-hoc way the tactic(...) entry of tactic notations
because it is actually not interpreted as a generic argument but rather
as a proper tactic expression instead.
There is for now no syntax to pass any tactic argument to a given ML or
notation tactic, but this should come soon.
Also fixes bug #3849 en passant.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The definition of Vernacexpr.VernacDeclareTacticDefinition was changed.
The original definition allowed us to represent non-sensical value such as:
VernacDeclareTacticDefinition(Qualid ..., false, ...)
The new definition prevents that.
|
| | |
| |
| |
| | |
command is mapped.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Originally, "VernacTime" and "VernacRedirect" were defined like this:
type vernac_expr =
...
| VernacTime of vernac_list
| VernacRedirect of string * vernac_list
...
where
type vernac_list = located_vernac_expr list
Currently, that list always contained one and only one element.
So I propose changing the definition of these two variants in the following way:
| VernacTime of located_vernac_expr
| VernacRedirect of string * located_vernac_expr
which covers all our current needs and enforces the invariant
related to the number of commands that are part of the
"VernacTime" and "VernacRedirect" variants.
|
| | | |
|
| |\| |
|
| | | |
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
Collecting the bound variables is now done on the glob_constr, before
interpretation, so that only variables given explicitly by the user
are used for binding bound variables.
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
We artificially restrict the syntax though, because it is unclear of
what the semantics of several axioms in a row is, in particular about the
resolution of remaining evars.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- "Proof using p*" means: use p and any section var about p.
- Simplify the grammar/parser for proof using <expression>.
- Section variables with a body (let-in) are pulled in automatically
since they are safe to be used (add no extra quantification)
- automatic clear of "unused" section variables made optional:
Set Proof Using Clear Unused.
since clearing section hypotheses does not "always work" (e.g. hint
databases are not really cleaned)
- term_typing: trigger a "suggest proof using" message also for Let
theorems.
|
| | |
| |
| |
| |
| | |
These options can be set to a string value, but also unset.
Internal data is of type string option.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This option disallows "declare at first use" semantics for universe
variables (in @{}), forcing the declaration of _all_ universes appearing
in a definition when introducing it with syntax Definition/Inductive
foo@{i j k} .. The bound universes at the end of a definition/inductive
must be exactly those ones, no extras allowed currently.
Test-suite files using the old semantics just disable the option.
|
| |\| |
|
| | |
| |
| |
| |
| | |
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
|
| |\| |
|
| | | |
|
Pierre-Marie Pédrot
Hugo Herbelin
Matthieu Sozeau
Maxime Dénès
Matej Kosik
Enrico Tassi
Matthieu Sozeau