1 files changed, 37 insertions, 0 deletions
diff --git a/pretyping/misctypes.ml b/pretyping/misctypes.ml
new file mode 100644
index 000000000..c66c9b1b8
--- /dev/null
+++ b/pretyping/misctypes.ml
@@ -0,0 +1,37 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+
+(** Some utility types for parsing *)
+
+type 'a or_var =
+  | ArgArg of 'a
+  | ArgVar of lident
+
+type 'a and_short_name = 'a * lident option
+
+type 'a or_by_notation_r =
+  | AN of 'a
+  | ByNotation of (string * string option)
+
+type 'a or_by_notation = 'a or_by_notation_r CAst.t
+
+(* NB: the last string in [ByNotation] is actually a [Notation.delimiters],
+   but this formulation avoids a useless dependency. *)
+
+(** 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 *)