diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/indfun.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index be84f2ed44..b613a4b13c 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -149,7 +149,9 @@ let build_newrecursive (fun (env,impls) ((_,recname),bl,arityc,_) -> let arityc = Constrexpr_ops.prod_constr_expr arityc bl in let arity,ctx = Constrintern.interp_type env0 sigma arityc in - let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in + let evdref = ref (Evd.from_env env0) in + let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in + let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in (Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls)) (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = |