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
|
(************************************************************************)
(* * 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 Environ
open Constrexpr
open Typeclasses
(** Instance declaration *)
val declare_instance : ?warn:bool -> env -> Evd.evar_map ->
hint_info option -> Hints.hint_locality -> GlobRef.t -> unit
(** Declares the given global reference as an instance of its type.
Does nothing — or emit a “not-a-class” warning if the [warn] argument is set —
when said type is not a registered type class. *)
val existing_instance : ?loc:Loc.t -> Hints.hint_locality -> GlobRef.t -> Vernacexpr.hint_info_expr option -> unit
(** globality, reference, optional priority and pattern information *)
val new_instance_interactive
: locality:Hints.hint_locality
-> poly:bool
-> name_decl
-> local_binder_expr list
-> constr_expr
-> ?tac:unit Proofview.tactic
-> ?hook:(GlobRef.t -> unit)
-> Vernacexpr.hint_info_expr
-> (bool * constr_expr) option
-> lident * Declare.Proof.t
val new_instance
: locality:Hints.hint_locality
-> poly:bool
-> name_decl
-> local_binder_expr list
-> constr_expr
-> (bool * constr_expr)
-> ?hook:(GlobRef.t -> unit)
-> Vernacexpr.hint_info_expr
-> lident
val new_instance_program
: locality:Hints.hint_locality
-> pm:Declare.OblState.t
-> poly:bool
-> name_decl
-> local_binder_expr list
-> constr_expr
-> (bool * constr_expr) option
-> ?hook:(GlobRef.t -> unit)
-> Vernacexpr.hint_info_expr
-> Declare.OblState.t * lident
val declare_new_instance
: locality:Hints.hint_locality
-> program_mode:bool
-> poly:bool
-> ident_decl
-> local_binder_expr list
-> constr_expr
-> Vernacexpr.hint_info_expr
-> unit
val add_class : typeclass -> unit
type instance = {
class_name : GlobRef.t;
instance : GlobRef.t;
info : Typeclasses.hint_info;
locality : Hints.hint_locality;
}
module Event : sig
type t =
| NewClass of typeclass
| NewInstance of instance
end
(** Activated observers are called whenever a class or an instance are declared.
[register_observer] is to be called once per process for a given
string, unless [override] is [true]. The registered observer is not activated.
Activation state is part of the summary. It is up to the caller to
use libobject for persistence if desired.
*)
type observer
val register_observer : name:string -> ?override:bool -> (Event.t -> unit) -> observer
val activate_observer : observer -> unit
val deactivate_observer : observer -> unit
(** Setting opacity *)
val set_typeclass_transparency
: locality:Hints.hint_locality
-> Evaluable.t list
-> bool
-> unit
val set_typeclass_transparency_com
: locality:Hints.hint_locality
-> Libnames.qualid list
-> bool
-> unit
val set_typeclass_mode
: locality:Hints.hint_locality
-> GlobRef.t
-> Hints.hint_mode list
-> unit
(** For generation on names based on classes only *)
val refine_att : bool Attributes.attribute
(** {6 Low level interface used by Add Morphism, do not use } *)
module Internal :
sig
val add_instance : typeclass -> hint_info -> Hints.hint_locality -> GlobRef.t -> unit
end
(** A configurable warning to output if a default mode is used for a class declaration. *)
val warn_default_mode : ?loc:Loc.t -> (GlobRef.t * Hints.hint_mode list) -> unit
|
