[api] Add compatiblity Misctypes module.

To be removed in 8.10.

3 files changed, 85 insertions, 0 deletions

diff --git a/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh b/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh
new file mode 100644
index 000000000..b4f716139
--- /dev/null
+++ b/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh
@@ -0,0 +1,8 @@
+_OVERLAY_BRANCH=misctypes+bye2
+
+if [ "$CI_PULL_REQUEST" = "7677" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then
+
+    Equations_CI_BRANCH="$_OVERLAY_BRANCH"
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/vernac/misctypes.ml b/vernac/misctypes.ml
new file mode 100644
index 000000000..ae725efaa
--- /dev/null
+++ b/vernac/misctypes.ml
@@ -0,0 +1,75 @@
+(* Compat module, to be removed in 8.10 *)
+open Names
+
+type lident = Names.lident
+[@@ocaml.deprecated "use [Names.lident"]
+type lname = Names.lname
+[@@ocaml.deprecated "use [Names.lname]"]
+type lstring = Names.lstring
+[@@ocaml.deprecated "use [Names.lstring]"]
+
+type 'a or_by_notation_r = 'a Constrexpr.or_by_notation_r =
+  | AN of 'a [@ocaml.deprecated "use version in [Constrexpr]"]
+  | ByNotation of (string * string option) [@ocaml.deprecated "use version in [Constrexpr]"]
+[@@ocaml.deprecated "use [Constrexpr.or_by_notation_r]"]
+
+type 'a or_by_notation = 'a Constrexpr.or_by_notation
+[@@ocaml.deprecated "use [Constrexpr.or_by_notation]"]
+
+type intro_pattern_naming_expr = Namegen.intro_pattern_naming_expr =
+  | IntroIdentifier of Id.t [@ocaml.deprecated "Use version in [Evarutil]"]
+  | IntroFresh of Id.t [@ocaml.deprecated "Use version in [Evarutil]"]
+  | IntroAnonymous [@ocaml.deprecated "Use version in [Evarutil]"]
+[@@ocaml.deprecated "use [Evarutil.intro_pattern_naming_expr]"]
+
+type 'a or_var = 'a Locus.or_var =
+  | ArgArg of 'a [@ocaml.deprecated "Use version in [Locus]"]
+  | ArgVar of Names.lident [@ocaml.deprecated "Use version in [Locus]"]
+[@@ocaml.deprecated "use [Locus.or_var]"]
+
+type quantified_hypothesis = Tactypes.quantified_hypothesis =
+    AnonHyp of int [@ocaml.deprecated "Use version in [Tactypes]"]
+  | NamedHyp of Id.t [@ocaml.deprecated "Use version in [Tactypes]"]
+[@@ocaml.deprecated "use [Tactypes.quantified_hypothesis]"]
+
+type multi = Equality.multi =
+  | Precisely of int [@ocaml.deprecated "use version in [Equality]"]
+  | UpTo of int [@ocaml.deprecated "use version in [Equality]"]
+  | RepeatStar [@ocaml.deprecated "use version in [Equality]"]
+  | RepeatPlus [@ocaml.deprecated "use version in [Equality]"]
+[@@ocaml.deprecated "use [Equality.multi]"]
+
+type 'a bindings = 'a Tactypes.bindings =
+  | ImplicitBindings of 'a list [@ocaml.deprecated "use version in [Tactypes]"]
+  | ExplicitBindings of 'a Tactypes.explicit_bindings [@ocaml.deprecated "use version in [Tactypes]"]
+  | NoBindings [@ocaml.deprecated "use version in [Tactypes]"]
+[@@ocaml.deprecated "use [Tactypes.bindings]"]
+
+type 'constr intro_pattern_expr = 'constr Tactypes.intro_pattern_expr =
+  | IntroForthcoming of bool [@ocaml.deprecated "use version in [Tactypes]"]
+  | IntroNaming of Namegen.intro_pattern_naming_expr [@ocaml.deprecated "use version in [Tactypes]"]
+  | IntroAction of 'constr Tactypes.intro_pattern_action_expr [@ocaml.deprecated "use version in [Tactypes]"]
+and 'constr intro_pattern_action_expr = 'constr Tactypes.intro_pattern_action_expr =
+  | IntroWildcard [@ocaml.deprecated "use [Tactypes]"]
+  | IntroOrAndPattern of 'constr Tactypes.or_and_intro_pattern_expr [@ocaml.deprecated "use [Tactypes]"]
+  | IntroInjection of ('constr intro_pattern_expr) CAst.t list [@ocaml.deprecated "use [Tactypes]"]
+  | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t [@ocaml.deprecated "use [Tactypes]"]
+  | IntroRewrite of bool [@ocaml.deprecated "use [Tactypes]"]
+and 'constr or_and_intro_pattern_expr = 'constr Tactypes.or_and_intro_pattern_expr =
+  | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list [@ocaml.deprecated "use [Tactypes]"]
+  | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list [@ocaml.deprecated "use [Tactypes]"]
+[@@ocaml.deprecated "use version in [Tactypes]"]
+
+type 'id move_location = 'id Logic.move_location =
+  | MoveAfter of 'id [@ocaml.deprecated "use version in [Logic]"]
+  | MoveBefore of 'id [@ocaml.deprecated "use version in [Logic]"]
+  | MoveFirst [@ocaml.deprecated "use version in [Logic]"]
+  | MoveLast [@ocaml.deprecated "use version in [Logic]"]
+[@@ocaml.deprecated "use version in [Logic]"]
+
+type 'a cast_type = 'a Glob_term.cast_type =
+  | CastConv of 'a [@ocaml.deprecated "use version in [Glob_term]"]
+  | CastVM of 'a [@ocaml.deprecated "use version in [Glob_term]"]
+  | CastCoerce [@ocaml.deprecated "use version in [Glob_term]"]
+  | CastNative of 'a [@ocaml.deprecated "use version in [Glob_term]"]
+[@@ocaml.deprecated "use version in [Glob_term]"]
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 39c313ac7..356951b69 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -31,3 +31,5 @@ Vernacstate
 Mltop
 Topfmt
 Vernacentries
+
+Misctypes