aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/dp/dp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/dp/dp.ml')
-rw-r--r--plugins/dp/dp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index 00a76efa3..b025cea64 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -468,7 +468,7 @@ and axiomatize_body env r id d = match r with
| VarRef _ ->
assert false
| ConstRef c ->
- begin match (Global.lookup_constant c).const_body with
+ begin match body_of_constant (Global.lookup_constant c) with
| Some b ->
let b = force b in
let axioms =