diff options
Diffstat (limited to 'ltac/tacinterp.mli')
| -rw-r--r-- | ltac/tacinterp.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli index 92f12fc8f..8bb6ee4cd 100644 --- a/ltac/tacinterp.mli +++ b/ltac/tacinterp.mli @@ -18,14 +18,14 @@ val ltac_trace_info : ltac_trace Exninfo.t module Value : sig - type t = Val.t + type t = Geninterp.Val.t val of_constr : constr -> t val to_constr : t -> constr option val of_int : int -> t val to_int : t -> int option val to_list : t -> t list option val of_closure : Geninterp.interp_sign -> glob_tactic_expr -> t - val cast : 'a typed_abstract_argument_type -> Val.t -> 'a + val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a end (** Values for interpretation *) |