1 files changed, 28 insertions, 0 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index 1452bbc347..e4f595ac4a 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -108,3 +108,31 @@ type 'a or_by_notation =
 (** Kinds of modules *)
 
 type module_kind = Module | ModType | ModAny
+
+(** Various flags *)
+
+type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
+type evars_flag = bool     (* true = pose evars       false = fail on evars *)
+type rec_flag = bool       (* true = recursive        false = not recursive *)
+type advanced_flag = bool  (* true = advanced         false = basic *)
+type letin_flag = bool     (* true = use local def    false = use Leibniz *)
+type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+
+type multi =
+  | Precisely of int
+  | UpTo of int
+  | RepeatStar
+  | RepeatPlus
+
+type 'a core_destruction_arg =
+  | ElimOnConstr of 'a
+  | ElimOnIdent of Id.t Loc.located
+  | ElimOnAnonHyp of int
+
+type 'a destruction_arg =
+  clear_flag * 'a core_destruction_arg
+
+type inversion_kind =
+  | SimpleInversion
+  | FullInversion
+  | FullInversionClear