diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d6ad5575b..49f833590 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -771,7 +771,7 @@ let make_graph (f_ref:global_reference) = with_full_print (fun () -> (Constrextern.extern_constr false env body, Constrextern.extern_type false env - ((*FIXNE*) c_body.const_type) + ((*FIXNE*) Typeops.type_of_constant_type env c_body.const_type) ) ) () |