diff options
Diffstat (limited to 'plugins/funind')
-rw-r--r-- | plugins/funind/functional_principles_types.ml | 2 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index d5bff57af..076fba861 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -348,7 +348,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.universe_context ~names:[] ~extensible:true evd' in + let univs = Evd.to_universe_context evd' in let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in ignore( Declare.declare_constant diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 63896bb56..320f7c7f3 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1556,7 +1556,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 ctx = Evd.universe_context ~names:[] ~extensible:true evm in + let ctx = Evd.to_universe_context evm in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res in (* Refresh the global universes, now including those of _F *) |