| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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).
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We just reuse the same one weird old trick in CAMLP4 to compare keywords and
identifiers as tokens. Note though that the commit 982460743 does not fix the
keyword vs. identifier issue in CAMLP4, so that the corresponding test fails.
This means that since that commit, some code compiling with CAMLP5 does not
when using CAMLP4, making it a second-class citizen.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
The tactic_arg entry was essentially a hack to keep parsing constrs as tactic
arguments. We rather use tactic_top_or_arg as the true entry for tactic arguments
now.
|
| | | |
| | |
| | |
| | |
| | | |
This was redundant with the wit_uconstr generic argument, so there was no real
point on keeping it there.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
METAIDENT were idents of the form $foobar, only used in quotations.
Note that it removes two dollars in the Coq codebase! Guess I'm absolved
for the $(...) syntax.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
This will allow an easier landing of the rewriting of Genarg.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
- Being stricter on the ordinal suffix accepted (only st for 1, 21,
etc, nd for 2, 22, etc., etc.)
- Reporting when the suffix is not the expected one (rather than
considering that, e.g. 2st, is two tokens, a number then an identifier).
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
We also intepret it at toplevel as a true constr and push the resulting
evarmap in the current state.
|
| | | |
| | |
| | |
| | |
| | | |
to g_tactic.ml4 so as to leave room for "IntroPattern []" to mean
"no introduction".
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
The parsing rules were broken and disallowed tactic replacement of the form
Ltac ident ::= expr.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | | |
|
Pierre-Marie Pédrot
Hugo Herbelin
Matthieu Sozeau
Maxime Dénès
Matej Kosik
Guillaume Melquiond