diff options
Diffstat (limited to 'src/tac2interp.mli')
| -rw-r--r-- | src/tac2interp.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tac2interp.mli b/src/tac2interp.mli index f99008c506..18522c3c91 100644 --- a/src/tac2interp.mli +++ b/src/tac2interp.mli @@ -27,6 +27,6 @@ val set_env : environment -> Glob_term.unbound_ltac_var_map -> Glob_term.unbound exception LtacError of KerName.t * valexpr array (** Ltac2-defined exceptions seen from OCaml side *) -val val_exn : Exninfo.iexn Geninterp.Val.typ +val val_exn : Exninfo.iexn Tac2dyn.Val.tag (** Toplevel representation of OCaml exceptions. Invariant: no [LtacError] should be put into a value with tag [val_exn]. *) |