diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 10 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 6 |
4 files changed, 9 insertions, 11 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 12b68e208c..25a7675113 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -364,7 +364,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let univs = Evd.const_univ_entry ~poly:false evd' in + let univs = Evd.univ_entry ~poly:false evd' in let ce = Declare.definition_entry ~univs value in ignore( Declare.declare_constant diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 02964d7ba5..ba0a3bbb5c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -321,12 +321,10 @@ let build_constructors_of_type ind' argl = construct in let argl = - if List.is_empty argl - then - Array.to_list - (Array.init (cst_narg - npar) (fun _ -> mkGHole ()) - ) - else argl + if List.is_empty argl then + List.make cst_narg (mkGHole ()) + else + List.make npar (mkGHole ()) @ argl in let pat_as_term = mkGApp(mkGRef (ConstructRef(ind',i+1)),argl) 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..a8517e9ab1 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 @@ -1547,7 +1547,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in + let univs = Evd.univ_entry ~poly:false evd in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res in (* Refresh the global universes, now including those of _F *) |