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 | |
| 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.
| -rw-r--r-- | tactics/extraargs.ml4 | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 9946aea82a..98868e8f91 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -23,10 +23,15 @@ let create_generic_quotation name e wit = let inject (loc, v) = Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v) in Egramcoq.create_ltac_quotation name inject (e, None) +let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int +let () = create_generic_quotation "string" Pcoq.Prim.string Stdarg.wit_string + +let () = create_generic_quotation "ident" Pcoq.Prim.ident Constrarg.wit_ident +let () = create_generic_quotation "reference" Pcoq.Prim.reference Constrarg.wit_ref let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Constrarg.wit_uconstr let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Constrarg.wit_constr let () = create_generic_quotation "ipattern" Pcoq.Tactic.simple_intropattern Constrarg.wit_intro_pattern -let () = create_generic_quotation "int" Pcoq.Prim.integer Stdarg.wit_int +let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Constrarg.wit_open_constr let () = let inject (loc, v) = Tacexpr.Tacexp v in Egramcoq.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5) |