diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /tactics/auto.ml | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'tactics/auto.ml')
-rw-r--r-- | tactics/auto.ml | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 0c0d9bcf..d7de6c4f 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -module CVars = Vars - open Pp open Util open Names @@ -81,15 +79,14 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = let clenv, c = if poly then (** Refresh the instance of the hint *) - let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in - let map c = CVars.subst_univs_level_constr subst c in + let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in 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 map evd; + evd = Evd.map_metas emap evd; env = Proofview.Goal.env gl; } in clenv, emap c @@ -102,7 +99,7 @@ let unify_resolve poly flags ((c : raw_hint), clenv) = Proofview.Goal.enter begin fun gl -> let clenv, c = connect_hint_clenv poly c clenv gl in let clenv = clenv_unique_resolver ~flags clenv gl in - Clenvtac.clenv_refine false clenv + Clenvtac.clenv_refine clenv end let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h |