Removing external uses of Val.inject and making Geninterp.interp return Val.t

4 files changed, 17 insertions, 17 deletions

diff --git a/engine/geninterp.ml b/engine/geninterp.ml
index 9e866f0cf..a3e494f5c 100644
--- a/engine/geninterp.ml
+++ b/engine/geninterp.ml
@@ -93,5 +93,9 @@ end
 
 module Interp = Register(InterpObj)
 
-let interp = Interp.obj
+let interp wit ist v =
+  let f = Interp.obj wit in
+  let tag = val_tag (Topwit wit) in
+  Ftactic.bind (f ist v) (fun v -> Ftactic.return (Val.inject tag v))
+
 let register_interp0 = Interp.register0
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
index 3c87b2512..c92181027 100644
--- a/engine/geninterp.mli
+++ b/engine/geninterp.mli
@@ -61,7 +61,7 @@ type interp_sign = {
 
 type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
 
-val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun
+val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun
 
 val register_interp0 :
   ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index da4ddd458..a3e6e0ebe 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -66,7 +66,12 @@ let prj : type a. a Val.typ -> Val.t -> a option = fun t v ->
 let in_list tag v =
   let tag = match tag with Val.Base tag -> tag | _ -> assert false in
   Val.Dyn (Val.list_tag, List.map (fun x -> Val.Dyn (tag, x)) v)
-let in_gen wit v = Val.inject (val_tag wit) v
+let in_gen wit v =
+  let t = match val_tag wit with
+  | Val.Base t -> t
+  | _ -> assert false (** not used in this module *)
+  in
+  Val.Dyn (t, v)
 let out_gen wit v =
   let t = match val_tag wit with
   | Val.Base t -> t
@@ -1143,17 +1148,6 @@ let rec read_match_rule lfun ist env sigma = function
   | [] -> []
 
 
-(* misc *)
-
-let interp_focussed wit f v =
-  Ftactic.nf_enter { enter = begin fun gl ->
-    let v = Genarg.out_gen (glbwit wit) v in
-    let env = Proofview.Goal.env gl in
-    let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
-    let v = in_gen (topwit wit) (f env sigma v) in
-    Ftactic.return v
-  end }
-
 (* Interprets an l-tac expression into a value *)
 let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftactic.t =
   (* The name [appl] of applied top-level Ltac names is ignored in
@@ -1568,8 +1562,7 @@ and interp_genarg ist x : Val.t Ftactic.t =
       interp_genarg ist (Genarg.in_gen (glbwit wit2) q) >>= fun q ->
       Ftactic.return (Val.Dyn (Val.pair_tag, (p, q)))
     | ExtraArg s ->
-      Geninterp.interp wit ist x >>= fun x ->
-      Ftactic.return (in_gen (Topwit wit) x)
+      Geninterp.interp wit ist x
 
 (** returns [true] for genargs which have the same meaning
     independently of goals. *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 46f484bf0..6b58baa99 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -156,7 +156,10 @@ let conclPattern concl pat tac =
        constr_bindings env sigma >>= fun constr_bindings ->
      let open Genarg in
      let open Geninterp in
-     let inj c = Val.inject (val_tag (topwit Constrarg.wit_constr)) c in
+     let inj c = match val_tag (topwit Constrarg.wit_constr) with
+     | Val.Base tag -> Val.Dyn (tag, c)
+     | _ -> assert false
+     in
      let fold id c accu = Id.Map.add id (inj c) accu in
      let lfun = Id.Map.fold fold constr_bindings Id.Map.empty in
      let ist = { lfun; extra = TacStore.empty } in