From 1dd682b1cafd64dd902e1ae6ea738192eb9b26db Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 2 Jun 2018 04:21:27 +0200 Subject: [api] Add compatiblity Misctypes module. To be removed in 8.10. --- vernac/misctypes.ml | 75 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 vernac/misctypes.ml (limited to 'vernac/misctypes.ml') 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]"] -- cgit v1.2.3