aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/classops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/classops.mli')
-rw-r--r--pretyping/classops.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 82af9d418..8f36e95e6 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -65,7 +65,7 @@ val class_args_of : env -> evar_map -> types -> constr list
(** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *)
val declare_coercion :
- coe_typ -> locality -> isid:bool ->
+ coe_typ -> ?local:bool -> isid:bool ->
src:cl_typ -> target:cl_typ -> params:int -> unit
(** {6 Access to coercions infos } *)