From 18a5eb4ecfcb7c2fbb315719c09e3d5fc0a3574e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Mar 2016 16:56:08 +0100
Subject: 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.
---
 tactics/extraargs.ml4 | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

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)
-- 
cgit v1.2.3