aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/ground.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/ground.ml')
-rw-r--r--plugins/firstorder/ground.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 6c1709140..e0f4fa95f 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -18,7 +18,7 @@ let update_flags ()=
let predref=ref Names.Cpred.empty in
let f coe=
try
- let kn=destConst (Classops.get_coercion_value coe) in
+ let kn= fst (destConst (Classops.get_coercion_value coe)) in
predref:=Names.Cpred.add kn !predref
with DestKO -> ()
in