removed t_app_infer_inst from term.ml

src/core/term.ml

@@ -721,10 +721,6 @@ let t_app_infer ls tl =
   let s = ls_arg_inst ls tl in
   t_app ls tl (oty_inst s ls.ls_value)
 
-let t_app_infer_inst ls tl ty =
-  let s = ls_arg_inst ls tl in
-  t_app ls tl (oty_inst s ty)
-
 let t_app ls tl ty = ignore (ls_app_inst ls tl ty); t_app ls tl ty
 
 let fs_app fs tl ty = t_app fs tl (Some ty)

src/core/term.mli

@@ -203,11 +203,6 @@ val t_app_infer : lsymbol -> term list -> term
 val ls_arg_inst : lsymbol -> term list -> ty Mtv.t
 val ls_app_inst : lsymbol -> term list -> ty option -> ty Mtv.t
 
-val t_app_infer_inst : lsymbol -> term list -> ty option ->term
-(** [t_app_infer_inst ls tl ty] builds the application of
-    symbol [ls] to arguments [tl], enforcing the result type to
-    an instance of type [ty] *)
-
 val t_var : vsymbol -> term
 val t_const : Number.constant -> term
 val t_if : term -> term -> term -> term

src/whyml/mlw_interp.ml

@@ -3,6 +3,10 @@ open Format
 
 open Term
 
+let t_app_infer_inst ls tl ty =
+  let s = ls_arg_inst ls tl in
+  t_app ls tl (Ty.oty_inst s ty)
+
 (* environment *)
 
 open Mlw_ty