diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 13 | ||||
| -rw-r--r-- | tactics/evar_tactics.ml | 5 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 4 |
3 files changed, 14 insertions, 8 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index f9b180de6c..6caebf6c4f 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -82,11 +82,14 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in let map c = Vars.subst_univs_level_constr subst c in let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in - let clenv = { clenv with evd = evd ; env = Proofview.Goal.env gl } in - (** FIXME: We're being inefficient here because we substitute the whole - evar map instead of just its metas, which are the only ones - mentioning the old universes. *) - Clenv.map_clenv map clenv, map c + (** Only metas are mentioning the old universes. *) + let clenv = { + templval = Evd.map_fl map clenv.templval; + templtyp = Evd.map_fl map clenv.templtyp; + evd = Evd.map_metas map evd; + env = Proofview.Goal.env gl; + } in + clenv, map c else let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in { clenv with evd = evd ; env = Proofview.Goal.env gl }, c diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 48b9006cd9..97b5ba0cc5 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -71,8 +71,11 @@ let instantiate_tac_by_name id c = let let_evar name typ = let src = (Loc.ghost,Evar_kinds.GoalEvar) in Proofview.Goal.s_enter { s_enter = begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in + let sigma = ref sigma in + let _ = Typing.sort_of env sigma typ in + let sigma = Sigma.Unsafe.of_evar_map !sigma in let id = match name with | Names.Anonymous -> let id = Namegen.id_of_name_using_hdchar env typ name in diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index d14e7deffd..29002af9e0 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1707,7 +1707,7 @@ let rec strategy_of_ast = function let mkappc s l = CAppExpl (Loc.ghost,(None,(Libnames.Ident (Loc.ghost,Id.of_string s)),None),l) let declare_an_instance n s args = - ((Loc.ghost,Name n), Explicit, + (((Loc.ghost,Name n),None), Explicit, CAppExpl (Loc.ghost, (None, Qualid (Loc.ghost, qualid_of_string s),None), args)) @@ -1923,7 +1923,7 @@ let add_morphism glob binders m s n = let poly = Flags.is_universe_polymorphism () in let instance_id = add_suffix n "_Proper" in let instance = - ((Loc.ghost,Name instance_id), Explicit, + (((Loc.ghost,Name instance_id),None), Explicit, CAppExpl (Loc.ghost, (None, Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), [cHole; s; m])) |