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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Names
(** Basic types used both in [constr_expr] and in [glob_constr] *)
(** Cases pattern variables *)
type patvar = Id.t
(** Introduction patterns *)
type 'constr intro_pattern_expr =
| IntroForthcoming of bool
| IntroNaming of intro_pattern_naming_expr
| IntroAction of 'constr intro_pattern_action_expr
and intro_pattern_naming_expr =
| IntroIdentifier of Id.t
| IntroFresh of Id.t
| IntroAnonymous
and 'constr intro_pattern_action_expr =
| IntroWildcard
| IntroOrAndPattern of 'constr or_and_intro_pattern_expr
| IntroInjection of ('constr intro_pattern_expr) Loc.located list
| IntroApplyOn of 'constr Loc.located * 'constr intro_pattern_expr Loc.located
| IntroRewrite of bool
and 'constr or_and_intro_pattern_expr =
| IntroOrPattern of ('constr intro_pattern_expr) Loc.located list list
| IntroAndPattern of ('constr intro_pattern_expr) Loc.located list
(** Move destination for hypothesis *)
type 'id move_location =
| MoveAfter of 'id
| MoveBefore of 'id
| MoveFirst
| MoveLast (** can be seen as "no move" when doing intro *)
(** Sorts *)
type 'a glob_sort_gen =
| GProp (** representation of [Prop] literal *)
| GSet (** representation of [Set] literal *)
| GType of 'a (** representation of [Type] literal *)
type sort_info = Name.t Loc.located list
type level_info = Name.t Loc.located option
type glob_sort = sort_info glob_sort_gen
type glob_level = level_info glob_sort_gen
type glob_constraint = glob_level * Univ.constraint_type * glob_level
(** A synonym of [Evar.t], also defined in Term *)
type existential_key = Evar.t
(** Case style, shared with Term *)
type case_style = Constr.case_style =
| LetStyle
| IfStyle
| LetPatternStyle
| MatchStyle
| RegularStyle (** infer printing form from number of constructor *)
[@@ocaml.deprecated "Alias for Constr.case_style"]
(** Casts *)
type 'a cast_type =
| CastConv of 'a
| CastVM of 'a
| CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
| CastNative of 'a
(** Bindings *)
type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t
type 'a explicit_bindings = (quantified_hypothesis * 'a) Loc.located list
type 'a bindings =
| ImplicitBindings of 'a list
| ExplicitBindings of 'a explicit_bindings
| NoBindings
type 'a with_bindings = 'a * 'a bindings
(** Some utility types for parsing *)
type 'a or_var =
| ArgArg of 'a
| ArgVar of Names.Id.t Loc.located
type 'a and_short_name = 'a * Id.t Loc.located option
type 'a or_by_notation =
| AN of 'a
| ByNotation of (string * string option) Loc.located
(* NB: the last string in [ByNotation] is actually a [Notation.delimiters],
but this formulation avoids a useless dependency. *)
(** Kinds of modules *)
type module_kind = Module | ModType | ModAny
(** 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 *)
type multi =
| Precisely of int
| UpTo of int
| RepeatStar
| RepeatPlus
type 'a core_destruction_arg =
| ElimOnConstr of 'a
| ElimOnIdent of Id.t Loc.located
| ElimOnAnonHyp of int
type 'a destruction_arg =
clear_flag * 'a core_destruction_arg
type inversion_kind =
| SimpleInversion
| FullInversion
| FullInversionClear
type ('a, 'b) gen_universe_decl = {
univdecl_instance : 'a; (* Declared universes *)
univdecl_extensible_instance : bool; (* Can new universes be added *)
univdecl_constraints : 'b; (* Declared constraints *)
univdecl_extensible_constraints : bool (* Can new constraints be added *) }