Rolling our own generic arguments.

13 files changed, 160 insertions, 93 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 672db12f1d..4e62fab715 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -86,11 +86,11 @@ let tac2mode = Gram.entry_create "vernac:ltac2_command"
 (** FUCK YOU API *)
 let ltac1_expr = (Obj.magic Pltac.tactic_expr : Tacexpr.raw_tactic_expr Gram.entry)
 
-let inj_wit wit loc x = CTacExt (loc, Genarg.in_gen (Genarg.rawwit wit) x)
-let inj_open_constr loc c = inj_wit Stdarg.wit_open_constr loc c
+let inj_wit wit loc x = CTacExt (loc, 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 Tacarg.wit_tactic loc e
+let inj_ltac1 loc e = inj_wit Tac2env.wit_ltac1 loc e
 
 let pattern_of_qualid loc id =
   if Tac2env.is_constructor (snd id) then CPatRef (loc, RelId id, [])
diff --git a/src/tac2core.ml b/src/tac2core.ml
index e865c1378f..cbc7c4744e 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -70,9 +70,6 @@ let of_rec_declaration (nas, ts, cs) =
   Value.of_array Value.of_constr ts,
   Value.of_array Value.of_constr cs)
 
-let val_valexpr : valexpr Val.tag = Val.create "ltac2:valexpr"
-let val_free : Id.Set.t Val.tag = Val.create "ltac2:free"
-
 (** Stdlib exceptions *)
 
 let err_notfocussed =
@@ -601,16 +598,16 @@ end
 (** Fresh *)
 
 let () = define2 "fresh_free_union" begin fun set1 set2 ->
-  let set1 = Value.to_ext val_free set1 in
-  let set2 = Value.to_ext val_free set2 in
+  let set1 = Value.to_ext Value.val_free set1 in
+  let set2 = Value.to_ext Value.val_free set2 in
   let ans = Id.Set.union set1 set2 in
-  return (Value.of_ext val_free ans)
+  return (Value.of_ext Value.val_free ans)
 end
 
 let () = define1 "fresh_free_of_ids" begin fun ids ->
   let ids = Value.to_list Value.to_ident ids in
   let free = List.fold_right Id.Set.add ids Id.Set.empty in
-  return (Value.of_ext val_free free)
+  return (Value.of_ext Value.val_free free)
 end
 
 let () = define1 "fresh_free_of_constr" begin fun c ->
@@ -621,11 +618,11 @@ let () = define1 "fresh_free_of_constr" begin fun c ->
   | _ -> EConstr.fold sigma fold accu c
   in
   let ans = fold Id.Set.empty c in
-  return (Value.of_ext val_free ans)
+  return (Value.of_ext Value.val_free ans)
 end
 
 let () = define2 "fresh_fresh" begin fun avoid id ->
-  let avoid = Value.to_ext val_free avoid in
+  let avoid = Value.to_ext Value.val_free avoid in
   let id = Value.to_ident id in
   let nid = Namegen.next_ident_away_from id (fun id -> Id.Set.mem id avoid) in
   return (Value.of_ident nid)
@@ -659,7 +656,11 @@ let to_lvar ist =
   let lfun = Tac2interp.set_env ist Id.Map.empty in
   { empty_lvar with Glob_term.ltac_genargs = lfun }
 
-let interp_constr flags ist (c, _) =
+let intern_constr ist c =
+  let (_, (c, _)) = Genintern.intern Stdarg.wit_constr ist c in
+  c
+
+let interp_constr flags ist c =
   let open Pretyping in
   pf_apply begin fun env sigma ->
   Proofview.V82.wrap_exceptions begin fun () ->
@@ -672,56 +673,90 @@ let interp_constr flags ist (c, _) =
   end
 
 let () =
+  let intern = intern_constr in
   let interp ist c = interp_constr (constr_flags ()) ist c in
   let obj = {
     ml_type = t_constr;
+    ml_intern = intern;
+    ml_subst = Detyping.subst_glob_constr;
     ml_interp = interp;
   } in
-  define_ml_object Stdarg.wit_constr obj
+  define_ml_object Tac2env.wit_constr obj
 
 let () =
+  let intern = intern_constr in
   let interp ist c = interp_constr (open_constr_no_classes_flags ()) ist c in
   let obj = {
     ml_type = t_constr;
+    ml_intern = intern;
+    ml_subst = Detyping.subst_glob_constr;
     ml_interp = interp;
   } in
-  define_ml_object Stdarg.wit_open_constr obj
+  define_ml_object Tac2env.wit_open_constr obj
 
 let () =
   let interp _ id = return (ValExt (Value.val_ident, id)) in
   let obj = {
     ml_type = t_ident;
+    ml_intern = (fun _ id -> id);
     ml_interp = interp;
+    ml_subst = (fun _ id -> id);
   } in
-  define_ml_object Stdarg.wit_ident obj
+  define_ml_object Tac2env.wit_ident obj
 
 let () =
+  let intern ist c =
+    let _, pat = Constrintern.intern_constr_pattern ist.Genintern.genv ~as_type:false c in
+    pat
+  in
   let interp _ c = return (ValExt (Value.val_pattern, c)) in
   let obj = {
     ml_type = t_pattern;
+    ml_intern = intern;
     ml_interp = interp;
+    ml_subst = Patternops.subst_pattern;
   } in
   define_ml_object Tac2env.wit_pattern obj
 
 let () =
+  let intern ist qid = match qid with
+  | Libnames.Ident (_, id) -> Globnames.VarRef id
+  | Libnames.Qualid (loc, qid) ->
+    let gr =
+      try Nametab.locate qid
+      with Not_found ->
+        Nametab.error_global_not_found ?loc qid
+    in
+    gr
+  in
+  let subst s c = Globnames.subst_global_reference s c in
   let interp _ gr = return (Value.of_reference gr) in
   let obj = {
     ml_type = t_reference;
+    ml_intern = intern;
+    ml_subst = subst;
     ml_interp = interp;
   } in
   define_ml_object Tac2env.wit_reference obj
 
 let () =
+  let intern ist tac =
+    let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in
+    tac
+  in
   let interp _ tac =
     (** FUCK YOU API *)
     (Obj.magic Ltac_plugin.Tacinterp.eval_tactic tac : unit Proofview.tactic) >>= fun () ->
     return v_unit
   in
+  let subst s tac = Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac in
   let obj = {
     ml_type = t_unit;
+    ml_intern = intern;
+    ml_subst = subst;
     ml_interp = interp;
   } in
-  define_ml_object Ltac_plugin.Tacarg.wit_tactic obj
+  define_ml_object Tac2env.wit_ltac1 obj
 
 (** Ltac2 in terms *)
 
@@ -754,38 +789,6 @@ let () =
   in
   Geninterp.register_interp0 wit_ltac2 interp
 
-(** Patterns *)
-
-let () =
-  let intern ist c =
-    let _, pat = Constrintern.intern_constr_pattern ist.Genintern.genv ~as_type:false c in
-    ist, pat
-  in
-  Genintern.register_intern0 wit_pattern intern
-
-let () =
-  let subst s c = Patternops.subst_pattern s c in
-  Genintern.register_subst0 wit_pattern subst
-
-(** References *)
-
-let () =
-  let intern ist qid = match qid with
-  | Libnames.Ident (_, id) -> ist, Globnames.VarRef id
-  | Libnames.Qualid (loc, qid) ->
-    let gr =
-      try Nametab.locate qid
-      with Not_found ->
-        Nametab.error_global_not_found ?loc qid
-    in
-    ist, gr
-  in
-  Genintern.register_intern0 wit_reference intern
-
-let () =
-  let subst s c = Globnames.subst_global_reference s c in
-  Genintern.register_subst0 wit_reference subst
-
 (** Built-in notation scopes *)
 
 let add_scope s f =
@@ -806,7 +809,7 @@ let add_generic_scope s entry arg =
   let parse = function
   | [] ->
     let scope = Extend.Aentry entry in
-    let act x = CTacExt (dummy_loc, in_gen (rawwit arg) x) in
+    let act x = CTacExt (dummy_loc, arg, x) in
     Tac2entries.ScopeRule (scope, act)
   | _ -> scope_fail ()
   in
@@ -927,8 +930,8 @@ 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 Stdarg.wit_constr
-let () = add_generic_scope "open_constr" Pcoq.Constr.constr Stdarg.wit_open_constr
+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
 
 (** seq scope, a bit hairy *)
diff --git a/src/tac2dyn.ml b/src/tac2dyn.ml
index 3f4fbca712..896676f08b 100644
--- a/src/tac2dyn.ml
+++ b/src/tac2dyn.ml
@@ -6,4 +6,22 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+module Arg =
+struct
+  module DYN = Dyn.Make(struct end)
+  module Map = DYN.Map
+  type ('a, 'b) tag = ('a * 'b) DYN.tag
+  let eq = DYN.eq
+  let repr = DYN.repr
+  let create = DYN.create
+end
+
+module type Param = sig type ('raw, 'glb) t end
+
+module ArgMap (M : Param) =
+struct
+  type _ pack = Pack : ('raw, 'glb) M.t -> ('raw * 'glb) pack
+  include Arg.Map(struct type 'a t = 'a pack end)
+end
+
 module Val = Dyn.Make(struct end)
diff --git a/src/tac2dyn.mli b/src/tac2dyn.mli
index e4b18ba373..e995296840 100644
--- a/src/tac2dyn.mli
+++ b/src/tac2dyn.mli
@@ -8,4 +8,27 @@
 
 (** Dynamic arguments for Ltac2. *)
 
+module Arg :
+sig
+  type ('a, 'b) tag
+  val create : string -> ('a, 'b) tag
+  val eq : ('a1, 'b1) tag -> ('a2, 'b2) tag -> ('a1 * 'b1, 'a2 * 'b2) CSig.eq option
+  val repr : ('a, 'b) tag -> string
+end
+(** Arguments that are part of an AST. *)
+
+module type Param = sig type ('raw, 'glb) t end
+
+module ArgMap (M : Param) :
+sig
+  type _ pack = Pack : ('raw, 'glb) M.t -> ('raw * 'glb) pack
+  type t
+  val empty : t
+  val add : ('a, 'b) Arg.tag -> ('a * 'b) pack -> t -> t
+  val remove : ('a, 'b) Arg.tag -> t -> t
+  val find : ('a, 'b) Arg.tag -> t -> ('a * 'b) pack
+  val mem : ('a, 'b) Arg.tag -> t -> bool
+end
+
 module Val : Dyn.S
+(** Toplevel values *)
diff --git a/src/tac2env.ml b/src/tac2env.ml
index dd8a07ffc6..39821b1cb6 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -10,6 +10,7 @@ open CErrors
 open Util
 open Names
 open Libnames
+open Tac2dyn
 open Tac2expr
 
 type global_data = {
@@ -250,22 +251,31 @@ let shortest_qualid_of_projection kn =
   let sp = KNmap.find kn tab.tab_proj_rev in
   KnTab.shortest_qualid Id.Set.empty sp tab.tab_proj
 
-type 'a ml_object = {
+type ('a, 'b) ml_object = {
   ml_type : type_constant;
-  ml_interp : environment -> 'a -> valexpr Proofview.tactic;
+  ml_intern : Genintern.glob_sign -> 'a -> 'b;
+  ml_subst : Mod_subst.substitution -> 'b -> 'b;
+  ml_interp : environment -> 'b -> valexpr Proofview.tactic;
 }
 
 module MLTypeObj =
 struct
-  type ('a, 'b, 'c) obj = 'b ml_object
-  let name = "ltac2_ml_type"
-  let default _ = None
+  type ('a, 'b) t = ('a, 'b) ml_object
 end
 
-module MLType = Genarg.Register(MLTypeObj)
+module MLType = Tac2dyn.ArgMap(MLTypeObj)
 
-let define_ml_object t tpe = MLType.register0 t tpe
-let interp_ml_object t = MLType.obj t
+let ml_object_table = ref MLType.empty
+
+let define_ml_object t tpe =
+  ml_object_table := MLType.add t (MLType.Pack tpe) !ml_object_table
+
+let interp_ml_object t =
+  try
+    let MLType.Pack ans = MLType.find t !ml_object_table in
+    ans
+  with Not_found ->
+    CErrors.anomaly Pp.(str "Unknown object type " ++ str (Tac2dyn.Arg.repr t))
 
 (** Absolute paths *)
 
@@ -278,8 +288,13 @@ let std_prefix =
 (** Generic arguments *)
 
 let wit_ltac2 = Genarg.make0 "ltac2:value"
-let wit_pattern = Genarg.make0 "ltac2:pattern"
-let wit_reference = Genarg.make0 "ltac2:reference"
+
+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
diff --git a/src/tac2env.mli b/src/tac2env.mli
index 8a5fb531d8..0ab6543178 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -10,6 +10,7 @@ open Genarg
 open Names
 open Libnames
 open Nametab
+open Tac2dyn
 open Tac2expr
 
 (** Ltac2 global environment *)
@@ -104,13 +105,15 @@ val interp_primitive : ml_tactic_name -> ml_tactic
 
 (** {5 ML primitive types} *)
 
-type 'a ml_object = {
+type ('a, 'b) ml_object = {
   ml_type : type_constant;
-  ml_interp : environment -> 'a -> valexpr Proofview.tactic;
+  ml_intern : Genintern.glob_sign -> 'a -> 'b;
+  ml_subst : Mod_subst.substitution -> 'b -> 'b;
+  ml_interp : environment -> 'b -> valexpr Proofview.tactic;
 }
 
-val define_ml_object : ('a, 'b, 'c) genarg_type -> 'b ml_object -> unit
-val interp_ml_object : ('a, 'b, 'c) genarg_type -> 'b ml_object
+val define_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object -> unit
+val interp_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object
 
 (** {5 Absolute paths} *)
 
@@ -124,13 +127,21 @@ 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, Util.Empty.t) genarg_type
+val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern) Arg.tag
 
-val wit_reference : (reference, Globnames.global_reference, Util.Empty.t) genarg_type
+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/tac2expr.mli b/src/tac2expr.mli
index 0b02ba2656..ccff8e7756 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -104,7 +104,7 @@ type raw_tacexpr =
 | CTacRec of Loc.t * raw_recexpr
 | CTacPrj of Loc.t * raw_tacexpr * ltac_projection or_relid
 | CTacSet of Loc.t * raw_tacexpr * ltac_projection or_relid * raw_tacexpr
-| CTacExt of Loc.t * raw_generic_argument
+| CTacExt : Loc.t * ('a, _) Tac2dyn.Arg.tag * 'a -> raw_tacexpr
 
 and raw_taccase = raw_patexpr * raw_tacexpr
 
@@ -132,7 +132,7 @@ type glb_tacexpr =
 | GTacSet of type_constant * glb_tacexpr * int * glb_tacexpr
 | GTacOpn of ltac_constructor * glb_tacexpr list
 | GTacWth of glb_tacexpr open_match
-| GTacExt of glob_generic_argument
+| GTacExt : (_, 'a) Tac2dyn.Arg.tag * 'a -> glb_tacexpr
 | GTacPrm of ml_tactic_name * glb_tacexpr list
 
 (** {5 Parsing & Printing} *)
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index 61b6d56b6c..6fc3b2e0f2 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -28,6 +28,7 @@ let val_projection = Val.create "ltac2:projection"
 let val_univ = Val.create "ltac2:universe"
 let val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.tag =
   Val.create "ltac2:kont"
+let val_free : Names.Id.Set.t Val.tag = Val.create "ltac2:free"
 
 let extract_val (type a) (type b) (tag : a Val.tag) (tag' : b Val.tag) (v : b) : a =
 match Val.eq tag tag' with
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index 1ce163256d..33b1010213 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -82,3 +82,4 @@ val val_constructor : constructor Val.tag
 val val_projection : Projection.t Val.tag
 val val_univ : Univ.universe_level Val.tag
 val val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.tag
+val val_free : Id.Set.t Val.tag
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 02dfa1c08b..051b3af5c7 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -200,7 +200,7 @@ let loc_of_tacexpr = function
 | CTacRec (loc, _) -> loc
 | CTacPrj (loc, _, _) -> loc
 | CTacSet (loc, _, _, _) -> loc
-| CTacExt (loc, _) -> loc
+| CTacExt (loc, _, _) -> loc
 
 let loc_of_patexpr = function
 | CPatVar (loc, _) -> Option.default dummy_loc loc
@@ -769,17 +769,16 @@ let rec intern_rec env = function
   let ret = subst_type substf pinfo.pdata_ptyp in
   let r = intern_rec_with_constraint env r ret in
   (GTacSet (pinfo.pdata_type, e, pinfo.pdata_indx, r), GTypRef (Tuple 0, []))
-| CTacExt (loc, ext) ->
+| CTacExt (loc, tag, arg) ->
   let open Genintern in
-  let GenArg (Rawwit tag, _) = ext in
   let tpe = interp_ml_object tag in
   (** External objects do not have access to the named context because this is
       not stable by dynamic semantics. *)
   let genv = Global.env_of_context Environ.empty_named_context_val in
   let ist = empty_glob_sign genv in
   let ist = { ist with extra = Store.set ist.extra ltac2_env env } in
-  let (_, ext) = Flags.with_option Ltac_plugin.Tacintern.strict_check (fun () -> generic_intern ist ext) () in
-  (GTacExt ext, GTypRef (Other tpe.ml_type, []))
+  let arg = Flags.with_option Ltac_plugin.Tacintern.strict_check (fun () -> tpe.ml_intern ist arg) () in
+  (GTacExt (tag, arg), GTypRef (Other tpe.ml_type, []))
 
 and intern_rec_with_constraint env e exp =
   let loc = loc_of_tacexpr e in
@@ -1248,8 +1247,8 @@ let rec globalize ids e = match e with
   let p = get_projection0 p in
   let e' = globalize ids e' in
   CTacSet (loc, e, AbsKn p, e')
-| CTacExt (loc, arg) ->
-  let arg = pr_argument_type (genarg_tag arg) in
+| CTacExt (loc, tag, arg) ->
+  let arg = str (Tac2dyn.Arg.repr tag) in
   CErrors.user_err ~loc (str "Cannot globalize generic arguments of type" ++ spc () ++ arg)
 
 and globalize_case ids (p, e) =
@@ -1324,9 +1323,10 @@ let rec subst_expr subst e = match e with
   let e' = subst_expr subst e in
   let r' = subst_expr subst r in
   if kn' == kn && e' == e && r' == r then e0 else GTacSet (kn', e', p, r')
-| GTacExt ext ->
-  let ext' = Genintern.generic_substitute subst ext in
-  if ext' == ext then e else GTacExt ext'
+| GTacExt (tag, arg) ->
+  let tpe = interp_ml_object tag in
+  let arg' = tpe.ml_subst subst arg in
+  if arg' == arg then e else GTacExt (tag, arg')
 | GTacOpn (kn, el) as e0 ->
   let kn' = subst_kn subst kn in
   let el' = List.smartmap (fun e -> subst_expr subst e) el in
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index 3be95ac828..f458f6e81f 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -99,8 +99,7 @@ let rec interp ist = function
 | GTacPrm (ml, el) ->
   Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
   Tac2env.interp_primitive ml el
-| GTacExt e ->
-  let GenArg (Glbwit tag, e) = e in
+| GTacExt (tag, e) ->
   let tpe = Tac2env.interp_ml_object tag in
   tpe.Tac2env.ml_interp ist e
 
diff --git a/src/tac2print.ml b/src/tac2print.ml
index 29f78f251e..6943697b45 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -279,13 +279,9 @@ let pr_glbexpr_gen lvl c =
     in
     let c = pr_constructor kn in
     paren (hov 0 (c ++ spc () ++ (pr_sequence (pr_glbexpr E0) cl)))
-  | GTacExt arg ->
-    let GenArg (Glbwit tag, arg) = arg in
-    let name = match tag with
-    | ExtraArg tag -> ArgT.repr tag
-    | _ -> assert false
-    in
-    hov 0 (str name ++ str ":" ++ paren (Genprint.glb_print tag arg))
+  | GTacExt (tag, arg) ->
+    let name = Tac2dyn.Arg.repr tag in
+    hov 0 (str name ++ str ":" ++ paren (str "_")) (** FIXME *)
   | GTacPrm (prm, args) ->
     let args = match args with
     | [] -> mt ()
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index f87e370032..279ab53b67 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -65,7 +65,7 @@ let of_option ?loc f opt = match opt with
 
 let inj_wit ?loc wit x =
   let loc = Option.default dummy_loc loc in
-  CTacExt (loc, Genarg.in_gen (Genarg.rawwit wit) x)
+  CTacExt (loc, wit, x)
 
 let of_variable (loc, id) =
   let qid = Libnames.qualid_of_ident id in
@@ -77,15 +77,15 @@ let of_anti f = function
 | QExpr x -> f x
 | QAnti id -> of_variable id
 
-let of_ident (loc, id) = inj_wit ?loc Stdarg.wit_ident id
+let of_ident (loc, id) = inj_wit ?loc Tac2env.wit_ident id
 
 let of_constr c =
   let loc = Constrexpr_ops.constr_loc c in
-  inj_wit ?loc Stdarg.wit_constr c
+  inj_wit ?loc Tac2env.wit_constr c
 
 let of_open_constr c =
   let loc = Constrexpr_ops.constr_loc c in
-  inj_wit ?loc Stdarg.wit_open_constr c
+  inj_wit ?loc Tac2env.wit_open_constr c
 
 let of_bool ?loc b =
   let c = if b then coq_core "true" else coq_core "false" in