diff options
Diffstat (limited to 'src/tac2ffi.mli')
| -rw-r--r-- | src/tac2ffi.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli index 33b1010213..cf1d7e81a1 100644 --- a/src/tac2ffi.mli +++ b/src/tac2ffi.mli @@ -83,3 +83,7 @@ val val_projection : Projection.t Val.tag val val_univ : Univ.universe_level Val.tag val val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.tag val val_free : Id.Set.t Val.tag + +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]. *) |