diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 1de0f91d1..094d2e50f 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -120,9 +120,9 @@ let const_of_id id = let def_of_const t = match (Term.kind_of_term t) with Term.Const sp -> - (try (match (Global.lookup_constant sp) with - {Declarations.const_body=Some c} -> Declarations.force c - |_ -> assert false) + (try (match Declarations.body_of_constant (Global.lookup_constant sp) with + | Some c -> Declarations.force c + | _ -> assert false) with _ -> assert false) |_ -> assert false |