diff options
author | 2015-10-06 17:51:57 +0200 | |
---|---|---|
committer | 2015-10-06 17:51:57 +0200 | |
commit | c4db6fc1086d984fd983ff9a6797ad108d220b98 (patch) | |
tree | cb57e5b678218e2baad13184544e645fd2e22cf5 /toplevel | |
parent | 944c8de0bfe4048e0733a487e6388db4dfc9075a (diff) | |
parent | 840155eafd9607c7656c80770de1e2819fe56a13 (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/class.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 0e270f960..f925a2d07 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -186,8 +186,9 @@ let error_not_transparent source = let build_id_coercion idf_opt source poly = let env = Global.env () in - let vs, ctx = match source with - | CL_CONST sp -> Universes.fresh_global_instance env (ConstRef sp) + let sigma = Evd.from_env env in + let sigma, vs = match source with + | CL_CONST sp -> Evd.fresh_global env sigma (ConstRef sp) | _ -> error_not_transparent source in let c = match constant_opt_value_in env (destConst vs) with | Some c -> c @@ -208,8 +209,8 @@ let build_id_coercion idf_opt source poly = (* juste pour verification *) let _ = if not - (Reductionops.is_conv_leq env Evd.empty - (Typing.unsafe_type_of env Evd.empty val_f) typ_f) + (Reductionops.is_conv_leq env sigma + (Typing.unsafe_type_of env sigma val_f) typ_f) then errorlabstrm "" (strbrk "Cannot be defined as coercion (maybe a bad number of arguments).") @@ -218,13 +219,13 @@ let build_id_coercion idf_opt source poly = match idf_opt with | Some idf -> idf | None -> - let cl,u,_ = find_class_type Evd.empty t in + let cl,u,_ = find_class_type sigma t in Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - (definition_entry ~types:typ_f ~poly ~univs:(Univ.ContextSet.to_context ctx) + (definition_entry ~types:typ_f ~poly ~univs:(Evd.universe_context sigma) ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) in let decl = (constr_entry, IsDefinition IdentityCoercion) in |