diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 2c5dae1cde..863c9dc8d5 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,4 +1,3 @@ -open API open CErrors open Util open Names @@ -851,7 +850,7 @@ let make_graph (f_ref:global_reference) = in (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom!" - | Some body -> + | Some (body, _) -> let env = Global.env () in let sigma = Evd.from_env env in let extern_body,extern_type = |