summaryrefslogtreecommitdiff
path: root/vernac/class.mli
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
commit9ebf44d84754adc5b64fcf612c6816c02c80462d (patch)
treebf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /vernac/class.mli
parent9043add656177eeac1491a73d2f3ab92bec0013c (diff)
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'vernac/class.mli')
-rw-r--r--vernac/class.mli9
1 files changed, 4 insertions, 5 deletions
diff --git a/vernac/class.mli b/vernac/class.mli
index 33d31fe1..f7e837f3 100644
--- a/vernac/class.mli
+++ b/vernac/class.mli
@@ -10,19 +10,18 @@
open Names
open Classops
-open Globnames
(** Classes and coercions. *)
(** [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion
from [src] to [tg] *)
-val try_add_new_coercion_with_target : global_reference -> local:bool ->
+val try_add_new_coercion_with_target : GlobRef.t -> local:bool ->
Decl_kinds.polymorphic ->
source:cl_typ -> target:cl_typ -> unit
(** [try_add_new_coercion ref s] declares [ref], assumed to be of type
[(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *)
-val try_add_new_coercion : global_reference -> local:bool ->
+val try_add_new_coercion : GlobRef.t -> local:bool ->
Decl_kinds.polymorphic -> unit
(** [try_add_new_coercion_subclass cst s] expects that [cst] denotes a
@@ -34,7 +33,7 @@ val try_add_new_coercion_subclass : cl_typ -> local:bool ->
(** [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion
from [src] to [tg] where the target is inferred from the type of [ref] *)
-val try_add_new_coercion_with_source : global_reference -> local:bool ->
+val try_add_new_coercion_with_source : GlobRef.t -> local:bool ->
Decl_kinds.polymorphic -> source:cl_typ -> unit
(** [try_add_new_identity_coercion id s src tg] enriches the
@@ -47,4 +46,4 @@ val add_coercion_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook
val add_subclass_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook
-val class_of_global : global_reference -> cl_typ
+val class_of_global : GlobRef.t -> cl_typ