diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 9d3c0b4b46..1b12cd42ce 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1106,7 +1106,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let not_free_in_t id = not (is_free_in id t) in let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in - let evd = Evd.from_env ~ctx env in + let evd = Evd.from_ctx ctx in let type_t' = Typing.unsafe_type_of env evd t' in let new_env = Environ.push_rel (n,Some t',type_t') env in let new_b,id_to_exclude = diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 65dc51a84f..eadeebd38e 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -597,7 +597,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in let ((_,_,typel),ctx,_) = Command.interp_fixpoint fixl ntns in let constr_expr_typel = - with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_env ~ctx (Global.env ())))) typel in + with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx))) 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 -> |