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 f0f76860a..609e2916d 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -766,9 +766,8 @@ let make_graph (f_ref:global_reference) = Dumpglob.pause (); (match body_of_constant c_body with | None -> error "Cannot build a graph over an axiom !" - | Some b -> + | Some body -> let env = Global.env () in - let body = Lazyconstr.force b in let extern_body,extern_type = with_full_print (fun () -> |