blob: ef9cd3c351316c6d43509f7fa14c760abdab7555 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
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 [Namegen]"]
| IntroFresh of Id.t [@ocaml.deprecated "Use version in [Namegen]"]
| IntroAnonymous [@ocaml.deprecated "Use version in [Namegen]"]
[@@ocaml.deprecated "use [Namegen.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]"]
|
