diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-09 14:00:42 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2017-09-19 10:28:03 +0200 |
| commit | cd29948855c2cbd3f4065170e41f8dbe625e1921 (patch) | |
| tree | e747c92a12074f2d0753b902c5fe00261d0a0fe4 /plugins/funind/functional_principles_types.ml | |
| parent | c2b881aae9c71a34199d2c66282512f2bdb19cf6 (diff) | |
Don't lose names in UState.universe_context.
We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
Diffstat (limited to 'plugins/funind/functional_principles_types.ml')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 15 |
1 files changed, 8 insertions, 7 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 |