Moving generic arguments to Tac2quote.

6 files changed, 45 insertions, 39 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 338711e79c..fce4c9e159 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -87,10 +87,10 @@ let tac2mode = Gram.entry_create "vernac:ltac2_command"
 let ltac1_expr = (Obj.magic Pltac.tactic_expr : Tacexpr.raw_tactic_expr Gram.entry)
 
 let inj_wit wit loc x = Loc.tag ~loc @@ CTacExt (wit, x)
-let inj_open_constr loc c = inj_wit Tac2env.wit_open_constr loc c
-let inj_pattern loc c = inj_wit Tac2env.wit_pattern loc c
-let inj_reference loc c = inj_wit Tac2env.wit_reference loc c
-let inj_ltac1 loc e = inj_wit Tac2env.wit_ltac1 loc e
+let inj_open_constr loc c = inj_wit Tac2quote.wit_open_constr loc c
+let inj_pattern loc c = inj_wit Tac2quote.wit_pattern loc c
+let inj_reference loc c = inj_wit Tac2quote.wit_reference loc c
+let inj_ltac1 loc e = inj_wit Tac2quote.wit_ltac1 loc e
 
 let pattern_of_qualid ?loc id =
   if Tac2env.is_constructor (snd id) then Loc.tag ?loc @@ CPatRef (RelId id, [])
diff --git a/src/tac2core.ml b/src/tac2core.ml
index db8f989768..f5dd74d642 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -803,7 +803,7 @@ let () =
     ml_interp = interp;
     ml_print = print;
   } in
-  define_ml_object Tac2env.wit_constr obj
+  define_ml_object Tac2quote.wit_constr obj
 
 let () =
   let intern = intern_constr in
@@ -815,7 +815,7 @@ let () =
     ml_interp = interp;
     ml_print = print;
   } in
-  define_ml_object Tac2env.wit_open_constr obj
+  define_ml_object Tac2quote.wit_open_constr obj
 
 let () =
   let interp _ id = return (ValExt (Value.val_ident, id)) in
@@ -826,7 +826,7 @@ let () =
     ml_subst = (fun _ id -> id);
     ml_print = print;
   } in
-  define_ml_object Tac2env.wit_ident obj
+  define_ml_object Tac2quote.wit_ident obj
 
 let () =
   let intern self ist c =
@@ -841,7 +841,7 @@ let () =
     ml_subst = Patternops.subst_pattern;
     ml_print = print;
   } in
-  define_ml_object Tac2env.wit_pattern obj
+  define_ml_object Tac2quote.wit_pattern obj
 
 let () =
   let intern self ist qid = match qid with
@@ -867,7 +867,7 @@ let () =
     ml_interp = interp;
     ml_print = print;
   } in
-  define_ml_object Tac2env.wit_reference obj
+  define_ml_object Tac2quote.wit_reference obj
 
 let () =
   let intern self ist tac =
@@ -892,7 +892,7 @@ let () =
     ml_interp = interp;
     ml_print = print;
   } in
-  define_ml_object Tac2env.wit_ltac1 obj
+  define_ml_object Tac2quote.wit_ltac1 obj
 
 (** Ltac2 in terms *)
 
@@ -1070,9 +1070,9 @@ let () = add_expr_scope "dispatch" q_dispatch Tac2quote.of_dispatch
 let () = add_expr_scope "strategy" q_strategy_flag Tac2quote.of_strategy_flag
 let () = add_expr_scope "reference" q_reference Tac2quote.of_reference
 
-let () = add_generic_scope "constr" Pcoq.Constr.constr wit_constr
-let () = add_generic_scope "open_constr" Pcoq.Constr.constr wit_open_constr
-let () = add_generic_scope "pattern" Pcoq.Constr.constr wit_pattern
+let () = add_generic_scope "constr" Pcoq.Constr.constr Tac2quote.wit_constr
+let () = add_generic_scope "open_constr" Pcoq.Constr.constr Tac2quote.wit_open_constr
+let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern
 
 (** seq scope, a bit hairy *)
 
diff --git a/src/tac2env.ml b/src/tac2env.ml
index 5a817df713..9aaaae0465 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -295,13 +295,6 @@ let std_prefix =
 
 let wit_ltac2 = Genarg.make0 "ltac2:value"
 
-let wit_pattern = Arg.create "pattern"
-let wit_reference = Arg.create "reference"
-let wit_ident = Arg.create "ident"
-let wit_constr = Arg.create "constr"
-let wit_open_constr = Arg.create "open_constr"
-let wit_ltac1 = Arg.create "ltac1"
-
 let is_constructor qid =
   let (_, id) = repr_qualid qid in
   let id = Id.to_string id in
diff --git a/src/tac2env.mli b/src/tac2env.mli
index eb18dc8e39..e40958e1a0 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -133,21 +133,6 @@ val std_prefix : ModPath.t
 
 val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type
 
-val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern) Arg.tag
-
-val wit_ident : (Id.t, Id.t) Arg.tag
-
-val wit_reference : (reference, Globnames.global_reference) Arg.tag
-(** Beware, at the raw level, [Qualid [id]] has not the same meaning as
-    [Ident id]. The first is an unqualified global reference, the second is
-    the dynamic reference to id. *)
-
-val wit_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag
-
-val wit_open_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag
-
-val wit_ltac1 : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr) Arg.tag
-
 (** {5 Helper functions} *)
 
 val is_constructor : qualid -> bool
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 063a52c738..132716c37e 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -9,9 +9,19 @@
 open Pp
 open Names
 open Util
+open Tac2dyn
 open Tac2expr
 open Tac2qexpr
 
+(** Generic arguments *)
+
+let wit_pattern = Arg.create "pattern"
+let wit_reference = Arg.create "reference"
+let wit_ident = Arg.create "ident"
+let wit_constr = Arg.create "constr"
+let wit_open_constr = Arg.create "open_constr"
+let wit_ltac1 = Arg.create "ltac1"
+
 (** Syntactic quoting of expressions. *)
 
 let control_prefix =
@@ -72,15 +82,15 @@ let of_anti f = function
 | QExpr x -> f x
 | QAnti id -> of_variable id
 
-let of_ident (loc, id) = inj_wit ?loc Tac2env.wit_ident id
+let of_ident (loc, id) = inj_wit ?loc wit_ident id
 
 let of_constr c =
   let loc = Constrexpr_ops.constr_loc c in
-  inj_wit ?loc Tac2env.wit_constr c
+  inj_wit ?loc wit_constr c
 
 let of_open_constr c =
   let loc = Constrexpr_ops.constr_loc c in
-  inj_wit ?loc Tac2env.wit_open_constr c
+  inj_wit ?loc wit_open_constr c
 
 let of_bool ?loc b =
   let c = if b then coq_core "true" else coq_core "false" in
@@ -270,7 +280,7 @@ let make_red_flag l =
 let of_reference r =
   let of_ref ref =
     let loc = Libnames.loc_of_reference ref in
-    inj_wit ?loc Tac2env.wit_reference ref
+    inj_wit ?loc wit_reference ref
   in
   of_anti of_ref r
 
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index b2687f01a3..440759ada7 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -8,6 +8,7 @@
 
 open Loc
 open Names
+open Tac2dyn
 open Tac2qexpr
 open Tac2expr
 
@@ -64,3 +65,20 @@ val of_exact_var : ?loc:Loc.t -> Id.t located -> raw_tacexpr
 val of_dispatch : dispatch -> raw_tacexpr
 
 val of_strategy_flag : strategy_flag -> raw_tacexpr
+
+(** {5 Generic arguments} *)
+
+val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern) Arg.tag
+
+val wit_ident : (Id.t, Id.t) Arg.tag
+
+val wit_reference : (Libnames.reference, Globnames.global_reference) Arg.tag
+(** Beware, at the raw level, [Qualid [id]] has not the same meaning as
+    [Ident id]. The first is an unqualified global reference, the second is
+    the dynamic reference to id. *)
+
+val wit_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag
+
+val wit_open_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag
+
+val wit_ltac1 : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr) Arg.tag