| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This was imposing a bit of useless burden on the API for no good reason.
|
|
This moves the typing code from the macro expansion to the extension
registering mechanism, bringing in more static safety. We also seize
the opportunity to remove dead code in the macro.
|
|
|
|
|
|
|
|
We remove the camlp4 compatibility layer, and try to clean up
most structures. `parsing/compat` is gone.
We added some documentation to the lexer/parser interfaces that are
often obscured by module includes.
|
|
|
|
|
|
Since TACTIC EXTEND relies on the usual tactic notation mechanism, the
interpretation of an ML tactic first goes through a TacAlias node. This
means that variables bound by the notation overwrite those of the current
environment. It turns out to be problematic for badly designed arguments
that close over variables of the environment, e.g. glob_constr, because
the variables used at interpretation time are now different from the ones
of parsing time.
Ideally, those arguments should return a closure made of the inner argument
together with the Ltac environment they were defined in. Unluckily, this would
need some important changes in their design. Most notably, most of ssreflect
ARGUMENT EXTEND actually create such closed arguments.
In order to emulate the old behaviour, we rather use a hack by prefixing
ML-bound variables by a character that is not accessible from user-side.
|
|
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 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.
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
With ocaml 4.01, the 'unused open' warning also checks the mli :-)
Beware: some open are reported as useless when compiling with camlp5,
but are necessary for compatibility with camlp4. These open are now
marked with a comment.
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15387 85f007b7-540e-0410-9357-904b9bb8a0f7
|
