aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-06-02 04:21:27 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-06-12 14:42:28 +0200
commit1dd682b1cafd64dd902e1ae6ea738192eb9b26db (patch)
treea95b931fbecc21f96099436f7ad6e4938f16c37d
parent615290d0f9d5cad7c508d45cf4ab89aecff033b2 (diff)
[api] Add compatiblity Misctypes module.
To be removed in 8.10.
-rw-r--r--dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh8
-rw-r--r--vernac/misctypes.ml75
-rw-r--r--vernac/vernac.mllib2
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