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
|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
open Glob_term
val map_glob_sort_gen : ('a -> 'b) -> 'a glob_sort_gen -> 'b glob_sort_gen
val glob_Type_sort : glob_sort
val glob_SProp_sort : glob_sort
val glob_Prop_sort : glob_sort
val glob_Set_sort : glob_sort
(** Equalities *)
val glob_sort_gen_eq : ('a -> 'a -> bool) -> 'a glob_sort_gen -> 'a glob_sort_gen -> bool
val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
val glob_qvar_eq : glob_qvar -> glob_qvar -> bool
val glob_quality_eq : glob_quality -> glob_quality -> bool
val glob_level_eq : Glob_term.glob_level -> Glob_term.glob_level -> bool
val relevance_info_eq : relevance_info -> relevance_info -> bool
val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
(** Expect a Prop/SProp/Set/Type universe; raise [ComplexSort] if
contains a max, an increment, or a flexible universe *)
exception ComplexSort
val glob_sort_quality : glob_sort -> UnivGen.QualityOrSet.t
val fresh_glob_sort_in_quality : Evd.evar_map -> glob_sort -> Evd.evar_map * Evd.esorts
val alias_of_pat : 'a cases_pattern_g -> Name.t
val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g
val cast_kind_eq : Constr.cast_kind -> Constr.cast_kind -> bool
val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool
(** Operations on [glob_constr] *)
val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option
val cases_predicate_names : 'a tomatch_tuples_g -> Name.t list
(** Apply a list of arguments to a glob_constr *)
val mkGApp : ?loc:Loc.t -> 'a glob_constr_g -> 'a glob_constr_g list -> 'a glob_constr_g
val map_glob_constr :
(glob_constr -> glob_constr) -> glob_constr -> glob_constr
(** Equality on [binding_kind] *)
val binding_kind_eq : binding_kind -> binding_kind -> bool
(** Ensure traversal from left to right *)
val map_glob_constr_left_to_right :
(glob_constr -> glob_constr) -> glob_constr -> glob_constr
val map_glob_constr_left_to_right_with_names :
(glob_constr -> glob_constr) -> (Name.t -> Name.t) -> glob_constr -> glob_constr
val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit
val mk_glob_constr_eq : (glob_constr -> glob_constr -> bool) ->
(Name.t -> Name.t -> glob_constr option -> glob_constr option -> bool) ->
glob_constr -> glob_constr -> bool
val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b
val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
val occur_glob_constr : Id.t -> 'a glob_constr_g -> bool
val free_glob_vars : 'a glob_constr_g -> Id.Set.t
val bound_glob_vars : glob_constr -> Id.Set.t
(* Obsolete *)
val loc_of_glob_constr : 'a glob_constr_g -> Loc.t option
val glob_visible_short_qualid : 'a glob_constr_g -> Id.Set.t
(* Renaming free variables using a renaming map; fails with
[UnsoundRenaming] if applying the renaming would introduce
collision, as in, e.g., renaming [P x y] using substitution [(x,y)];
inner alpha-conversion done only for forall, fun, let but
not for cases and fix *)
exception UnsoundRenaming
val rename_var : (Id.t * Id.t) list -> Id.t -> Id.t
val rename_glob_vars : (Id.t * Id.t) list -> 'a glob_constr_g -> 'a glob_constr_g
(** [map_pattern_binders f m c] applies [f] to all the binding names
in a pattern-matching expression ({!Glob_term.GCases}) represented
here by its relevant components [m] and [c]. It is used to
interpret Ltac-bound names both in pretyping and printing of
terms. *)
val map_pattern_binders : (Name.t -> Name.t) ->
tomatch_tuples -> cases_clauses -> (tomatch_tuples*cases_clauses)
(** [map_pattern f m c] applies [f] to the return predicate and the
right-hand side of a pattern-matching expression
({!Glob_term.GCases}) represented here by its relevant components
[m] and [c]. *)
val map_pattern : (glob_constr -> glob_constr) ->
tomatch_tuples -> cases_clauses -> (tomatch_tuples*cases_clauses)
(** Conversion from glob_constr to cases pattern, if possible
Evaluation is forced.
Take the current alias as parameter,
@raise Not_found if translation is impossible *)
val cases_pattern_of_glob_constr : Environ.env -> Name.t -> 'a glob_constr_g -> 'a cases_pattern_g
val glob_constr_of_closed_cases_pattern : Environ.env -> 'a cases_pattern_g -> Name.t * 'a glob_constr_g
(** A canonical encoding of cases pattern into constr such that
composed with [cases_pattern_of_glob_constr Anonymous] gives identity *)
val glob_constr_of_cases_pattern : Environ.env -> 'a cases_pattern_g -> 'a glob_constr_g
val add_patterns_for_params_remove_local_defs : Environ.env -> constructor ->
'a cases_pattern_g list -> 'a cases_pattern_g list
val empty_lvar : Ltac_pretype.ltac_var_map
val kind_of_glob_kind : glob_evar_kind -> Evar_kinds.t
val naming_of_glob_kind : glob_evar_kind -> Namegen.intro_pattern_naming_expr
|
