diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 19:29:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 15:14:45 +0200 |
| commit | 001c95411b6674423886a085d8f624ea031a9ebc (patch) | |
| tree | 0be049a0094b90c95b7e0aa5a7b1b479c24f421e /pretyping/typeclasses.ml | |
| parent | 8b3978baa5ceb41aaec4d9864c878847b82682d7 (diff) | |
Safer API for Global.type_of_global_in_context.
We return the abstract context instead of an arbitrary instantiation.
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index bae831b63..6de5bc28b 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -279,8 +279,10 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i)) in let ty, ctx = Global.type_of_global_in_context env glob in + let inst, ctx = Universes.fresh_instance_from ctx None in + let ty = Vars.subst_instance_constr inst ty in let ty = EConstr.of_constr ty in - let sigma = Evd.merge_context_set Evd.univ_rigid sigma (Univ.ContextSet.of_context ctx) in + let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in let rec aux pri c ty path = match class_of_constr sigma ty with | None -> [] @@ -317,7 +319,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = hints @ (path', info, body) :: rest in List.fold_left declare_proj [] projs in - let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in + let term = Universes.constr_of_global_univ (glob, inst) in (*FIXME subclasses should now get substituted for each particular instance of the polymorphic superclass *) aux pri term ty [glob] |