diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3f14de282..18b96e765 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -875,7 +875,7 @@ let understand_judgment_tcc evdref env c = let ise_pretype_gen_ctx flags sigma env lvar kind c = let evd, c = ise_pretype_gen flags sigma env lvar kind c in let evd, f = Evarutil.nf_evars_and_universes evd in - f c, Evd.get_universe_context_set evd + f c, Evd.evar_universe_context evd (** Entry points of the high-level type synthesis algorithm *) |