diff options
| author | Pierre-Marie Pédrot | 2016-03-04 16:56:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-04 17:49:13 +0100 |
| commit | 18a5eb4ecfcb7c2fbb315719c09e3d5fc0a3574e (patch) | |
| tree | 91987abbeb9eb9ac1c26674740412550b80b19bd /kernel/nativecode.mli | |
| parent | cbc3a5f16871adb399689f7673a2a29a82dbf0cb (diff) | |
Adding some standard arguments in tactic scopes.
This is not perfect and repeats what we do in Pcoq, but it is hard to factorize
because rules defined in Pcoq do not have the same precedence. For instance,
constr as a Tactic Notation argument is a Pcoq.Constr.constr while as a
quotation argument is a Pcoq.Constr.lconstr. We should think of a fix in the
long run, but for now it is reasonable to duplicate code.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions