From 8e77752080b6f0da3ce396e7537db9676e848a70 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Mar 2016 15:55:02 +0100
Subject: Replacing ad-hoc tactic scopes by generic ones using
 [create_ltac_quotations].

---
 tactics/coretactics.ml4 |  2 ++
 tactics/extraargs.ml4   | 14 ++++++++++++++
 2 files changed, 16 insertions(+)

(limited to 'tactics')

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 74d98176a4..7da6df717e 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -19,6 +19,8 @@ open Sigma.Notations
 
 DECLARE PLUGIN "coretactics"
 
+(** Basic tactics *)
+
 TACTIC EXTEND reflexivity
   [ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
 END
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 8f336cdb30..9946aea82a 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -17,6 +17,20 @@ open Tacinterp
 open Misctypes
 open Locus
 
+(** Adding scopes for generic arguments not defined through ARGUMENT EXTEND *)
+
+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 "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 () =
+  let inject (loc, v) = Tacexpr.Tacexp v in
+  Egramcoq.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5)
+
 (* Rewriting orientation *)
 
 let _ = Metasyntax.add_token_obj "<-"
-- 
cgit v1.2.3