diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 953e1f049c..e2273972e7 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -538,7 +538,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in let ((_,_,typel),_,_) = Command.interp_fixpoint fixl ntns in let constr_expr_typel = - with_full_print (List.map (Constrextern.extern_constr false (Global.env ()))) typel in + with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) Evd.empty)) typel in let fixpoint_exprl_with_new_bl = List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> @@ -768,8 +768,8 @@ let make_graph (f_ref:global_reference) = let env = Global.env () in let extern_body,extern_type = with_full_print (fun () -> - (Constrextern.extern_constr false env body, - Constrextern.extern_type false env + (Constrextern.extern_constr false env Evd.empty body, + Constrextern.extern_type false env Evd.empty ((*FIXNE*) Typeops.type_of_constant_type env c_body.const_type) ) ) |