| Commit message (Collapse) | Author | Age |
... | |
| |
|
|\ |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
This reverts commit c4ce1baa9f66210ebc1909988b3dd8baa1b8ef27.
|
| |
| |
| |
| |
| |
| | |
EXTEND and""
This reverts commit eb9216e544cb5fce4347052f42e9452a822c2f64.
|
| |
| |
| |
| | |
This reverts commit fb1b7b084bcbbbc176040fcadeac00aee6b1e462.
|
| |
| |
| |
| | |
VERNAC EXTEND.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
The TYPED AS clause was useless when defining a fresh generic argument.
Instead of having to write it mandatorily, we simply make it optional.
|
| |
| |
| |
| |
| | |
This allows to use the ARGUMENT EXTEND macro while sharing the same
toplevel dynamic representation as another argument.
|
| |
| |
| |
| |
| |
| | |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
This fixes parsing conflicts with the [fix ... with] tactic.
|
| |
| |
| |
| |
| |
| |
| |
| | |
This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They
now have to be reachable in the ML code. Note that this has some consequences,
as the previous macro was potentially mixing grammar entries and arguments as
long as their name was the same. Now, each genarg comes with its grammar
instead, so there is no way to abuse the macro.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The ARGUMENT EXTEND macro was discriminating between parsing entries known
statically, i.e. defined in Pcoq and unknown entires. Although simplifying
a bit the life of the plugin writer, it made actual interpretation difficult
to predict and complicated the code of the ARGUMENT EXTEND macro.
After this patch, all parsing entries and generic arguments used in an
ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding
a few more "open Pcoq.X" and "open Constrarg" here and there.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| | |
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 ARGUMENT EXTEND statement was wrongly using a CompatLoc instead of a Loc,
and this was not detected by typing "thanks" to the Gram.action magic. When
using CAMLP4, this was wreaking havoc at runtime, but not when using CAMLP5,
as the locations where sharing the same representation.
|
| |
| |
| |
| |
| | |
Amongs other things, it kind of fixes bug #4492, even though you cannot really
take advantage of the parsed data for now.
|
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| | |
It implemented the quotation logic of terms and tactics, although it was
mostly obsolete. With quotations gone, it is now useless and thus removed.
I fundamentally doubt that anyone hardly depends on this out there.
|
| | |
|
|\| |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
|\|
| |
| |
| |
| | |
Conflicts:
lib/cSig.mli
|
| |
| |
| |
| |
| |
| |
| |
| | |
CString was linked after Serialize, although the later was using CString.equal.
This had not been noticed so far because OCaml was ignoring functions marked as
external in interfaces (which is the case of CString.equal) when considering
link dependencies. This was changed on the OCaml side as part of the fix of
PR#6956, so linking was now failing in several places.
|
| |
| |
| |
| | |
Actually the identifier was never used and just carried along.
|