Added a generic handler of Ltac quotations, based on the existing

syntax constr:foo and ipattern:bar (which is not very nice for
parsing, b.t.w.).

Now one is able to dynamically add quotations of the form name:...
that will use the provided function to create a dynamically typed
argument.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16611 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions