aboutsummaryrefslogtreecommitdiff
path: root/intf/misctypes.mli
diff options
context:
space:
mode:
Diffstat (limited to 'intf/misctypes.mli')
-rw-r--r--intf/misctypes.mli13
1 files changed, 13 insertions, 0 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index e7f8b1b2ac..97b4b45fe0 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -40,6 +40,19 @@ type 'id move_location =
type sort_info = string option
type glob_sort = GProp | GSet | GType of sort_info
+(** A synonym of [int], also defined in Term *)
+
+type existential_key = int
+
+(** Case style, shared with Term *)
+
+type case_style = Term.case_style =
+ | LetStyle
+ | IfStyle
+ | LetPatternStyle
+ | MatchStyle
+ | RegularStyle (** infer printing form from number of constructor *)
+
(** Casts *)
type 'a cast_type =