diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d9b0330e2b..42dc66dcf4 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -166,7 +166,7 @@ let build_newrecursive let arityc = Constrexpr_ops.mkCProdN bl arityc in let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evd = Evd.from_env env0 in - let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in + let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in let open Context.Named.Declaration in (EConstr.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 1b5286dce4..0c97f9f373 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1518,10 +1518,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let open CVars in let env = Global.env() in let evd = Evd.from_env env in - let evd, function_type = interp_type_evars env evd type_of_f in + let evd, function_type = interp_type_evars ~program_mode:false env evd type_of_f in let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) - let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in + let evd, ty = interp_type_evars ~program_mode:false env evd ~impls:rec_impls eq in let evd = Evd.minimize_universes evd in let equation_lemma_type = Reductionops.nf_betaiotazeta env evd (Evarutil.nf_evar evd ty) in let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in |