Removing the Value.of_* API for parameterized types.

Although still working, it is now bad practice to use it, and it is not
widely spread anyway.

3 files changed, 6 insertions, 11 deletions

diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index f39a42271b..da4ddd4586 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -63,6 +63,9 @@ let prj : type a. a Val.typ -> Val.t -> a option = fun t v ->
   | None -> None
   | Some Refl -> Some x
 
+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 out_gen wit v =
   let t = match val_tag wit with
@@ -1577,7 +1580,7 @@ and interp_genarg_constr_list ist x =
   let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
   let lc = Genarg.out_gen (glbwit (wit_list wit_constr)) x in
   let (sigma,lc) = interp_constr_list ist env sigma lc in
-  let lc = Value.of_list (val_tag wit_constr) lc in
+  let lc = in_list (val_tag wit_constr) lc in
   Sigma.Unsafe.of_pair (Ftactic.return lc, sigma)
   end }
 
@@ -1587,7 +1590,8 @@ and interp_genarg_var_list ist x =
   let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
   let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in
   let lc = interp_hyp_list ist env sigma lc in
-  Ftactic.return (Value.of_list (val_tag wit_var) lc)
+  let lc = in_list (val_tag wit_var) lc in
+  Ftactic.return lc
   end }
 
 (* Interprets tactic expressions : returns a "constr" *)
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index a03c529cc0..a6e7af16e9 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -86,16 +86,10 @@ let to_int v =
 
 let to_list v = prj Val.list_tag v
 
-let of_list t v = Val.Dyn (Val.list_tag, List.map (fun v -> Val.inject t v) v)
-
 let to_option v = prj Val.opt_tag v
 
-let of_option t v = Val.Dyn (Val.opt_tag, Option.map (fun v -> Val.inject t v) v)
-
 let to_pair v = prj Val.pair_tag v
 
-let of_pair t1 t2 (v1, v2) = Val.Dyn (Val.pair_tag, (Val.inject t1 v1, Val.inject t2 v2))
-
 end
 
 let is_variable env id =
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index 82e1910f7d..7a963f95f3 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -42,11 +42,8 @@ sig
   val of_int : int -> t
   val to_int : t -> int option
   val to_list : t -> t list option
-  val of_list : 'a Val.tag -> 'a list -> t
   val to_option : t -> t option option
-  val of_option : 'a Val.tag -> 'a option -> t
   val to_pair : t -> (t * t) option
-  val of_pair : 'a Val.tag -> 'b Val.tag -> ('a * 'b) -> t
 end
 
 (** {5 Coercion functions} *)