aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/discharge.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/discharge.ml')
-rw-r--r--toplevel/discharge.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 1eb74c7e7..d148a5343 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -253,7 +253,7 @@ let process_object oldenv olddir full_olddir newdir
((Class (y1,y2))::ops, ids_to_discard, work_alist)
| "COERCION" ->
- let (((_,coeinfo),_,_)as x) = outCoercion lobj in
+ let (_,coeinfo,_,_ as x) = outCoercion lobj in
if coercion_strength coeinfo = Local then
(ops,ids_to_discard,work_alist)
else