aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/ground.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 48e60d798..6c1709140 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -20,7 +20,8 @@ let update_flags ()=
try
let kn=destConst (Classops.get_coercion_value coe) in
predref:=Names.Cpred.add kn !predref
- with Invalid_argument "destConst"-> () in
+ with DestKO -> ()
+ in
List.iter f (Classops.coercions ());
red_flags:=
Closure.RedFlags.red_add_transparent