diff options
author | 2017-09-26 23:57:40 +0200 | |
---|---|---|
committer | 2017-09-26 23:57:40 +0200 | |
commit | b9740771e8113cb9e607793887be7a12587d0326 (patch) | |
tree | f69105ad9813738abd10ae824756947940a7dc6d /plugins/funind | |
parent | 4b6383889d4d38de4c9a28bee960b30114a51b16 (diff) | |
parent | 3c964a60d698134c21adc77cbb69ce1528350682 (diff) |
Merge PR #688: Binding universe constraints in Definition/Inductive/etc...
Diffstat (limited to 'plugins/funind')
-rw-r--r-- | plugins/funind/functional_principles_types.ml | 15 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 5 |
2 files changed, 12 insertions, 8 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index ef1654fdf..409bb89ee 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -338,13 +338,14 @@ let generate_functional_principle (evd: Evd.evar_map ref) then (* let id_of_f = Label.to_id (con_label f) in *) let register_with_sort fam_sort = - let evd' = Evd.from_env (Global.env ()) in - let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in - let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in - 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 ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in + let evd' = Evd.from_env (Global.env ()) in + let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in + let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in + 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 = (snd (Evd.universe_context ~names:[] ~extensible:true evd')) in + let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in ignore( Declare.declare_constant name diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 41a10cba3..d43fd78f3 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1543,7 +1543,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let equation_id = add_suffix function_name "_equation" in let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in - let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in + let functional_ref = + let ctx = (snd (Evd.universe_context ~names:[] ~extensible:true evm)) in + declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res + in (* Refresh the global universes, now including those of _F *) let evm = Evd.from_env (Global.env ()) in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in |