diff options
| -rw-r--r-- | tactics/class_tactics.ml | 7 | ||||
| -rw-r--r-- | tactics/hints.ml | 5 |
2 files changed, 4 insertions, 8 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 1fadc164bf..36544883aa 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -179,11 +179,8 @@ let unify_resolve_refine flags h diff = let ty = Retyping.get_type_of env sigma term in let sigma, cl = Clenv.make_evar_clause env sigma ?len ty in let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in - let sigma = - Evarconv.(unify_leq_delay - ~flags:(default_flags_of flags.core_unify_flags.modulo_delta) - env sigma cl.cl_concl concl) - in + let flags = Evarconv.default_flags_of flags.core_unify_flags.modulo_delta in + let sigma = Evarconv.unify_leq_delay ~flags env sigma cl.cl_concl concl in (sigma, term) end end diff --git a/tactics/hints.ml b/tactics/hints.ml index e029e4628d..7b203c3d51 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1608,13 +1608,12 @@ let connect_hint_clenv h gl = let emap c = 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 emap clenv.templval; templtyp = Evd.map_fl emap clenv.templtyp; evd = Evd.map_metas emap evd; env = Proofview.Goal.env gl; - } in - clenv + } else let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in { clenv with evd = evd ; env = Proofview.Goal.env gl } |