Imported Upstream version 8.9.0upstream/8.9.0upstream

1 files changed, 3 insertions, 2 deletions

diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index bd44bdbe..f9883e44 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -14,7 +14,7 @@ open EConstr
 open Tacexpr
 open Genarg
 open Redexpr
-open Misctypes
+open Tactypes
 
 val ltac_trace_info : ltac_trace Exninfo.t
 
@@ -28,6 +28,7 @@ sig
   val to_list : t -> t list option
   val of_closure : Geninterp.interp_sign -> glob_tactic_expr -> t
   val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a
+  val apply : t -> t list -> unit Proofview.tactic
 end
 
 (** Values for interpretation *)
@@ -131,7 +132,7 @@ val interp_ltac_var : (value -> 'a) -> interp_sign ->
 
 val interp_int : interp_sign -> lident -> int
 
-val interp_int_or_var : interp_sign -> int or_var -> int
+val interp_int_or_var : interp_sign -> int Locus.or_var -> int
 
 val default_ist : unit -> Geninterp.interp_sign
 (** Empty ist with debug set on the current value. *)