aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/classops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/classops.ml')
-rw-r--r--pretyping/classops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 73ce8134f..2d2677ee0 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -398,7 +398,7 @@ let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) =
let classify_coercion (coe,stre,isid,cls,clt,ps as obj) =
if stre = Local then Dispose else Substitute obj
-let (inCoercion,_) =
+let inCoercion =
declare_object {(default_object "COERCION") with
open_function = open_coercion;
load_function = load_coercion;