From 6f51b8cafe7a873600e7a0c8675a72a8aee40184 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 5 Oct 2015 10:29:37 +0200 Subject: Univs: fix handling of evar_map in identity coercion construction. --- toplevel/class.ml | 13 +++++++------ 1 file 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 -- cgit v1.2.3