diff options
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 7462b8d855..2b654f5634 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -84,11 +84,12 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = (** Refresh the instance of the hint *) let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in let map c = Vars.subst_univs_level_constr subst c in + let emap c = EConstr.Vars.subst_univs_level_constr subst c in let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in (** Only metas are mentioning the old universes. *) let clenv = { - templval = Evd.map_fl map clenv.templval; - templtyp = Evd.map_fl map clenv.templtyp; + templval = Evd.map_fl emap clenv.templval; + templtyp = Evd.map_fl emap clenv.templtyp; evd = Evd.map_metas map evd; env = Proofview.Goal.env gl; } in |