diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 99bf66d1f..fd4e23de7 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -8,6 +8,7 @@ open Libnames open Globnames open Glob_term open Declarations +open Declareops open Misctypes open Decl_kinds @@ -770,7 +771,7 @@ let make_graph (f_ref:global_reference) = | None -> error "Cannot build a graph over an axiom !" | Some b -> let env = Global.env () in - let body = (force b) in + let body = Lazyconstr.force b in let extern_body,extern_type = with_full_print (fun () -> |