diff options
| author | Pierre-Marie Pédrot | 2020-07-16 19:34:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-12 14:07:13 +0200 |
| commit | a666788182bce7059e6ba41b917b5ca6ab52ae13 (patch) | |
| tree | 00221510912864d8c6bb73c061b1a8478796f5bc /tactics | |
| parent | de16cf5411c2696044d5b17cccb3659d21a79921 (diff) | |
Code simplification around hint manipulation in Class_tactics.
We inline the clenv universe refreshing, since it was the only place in the
code that used it. Furthermore it was performing useless substitutions in
the clenv.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 6c1bdca682..279476badb 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -143,6 +143,12 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st = resolve_evars = false } +let refresh_undefined_univs clenv = + match EConstr.kind clenv.evd clenv.templval.rebus with + | Var _ -> clenv.evd, Univ.empty_level_subst + | App (f, args) when isVar clenv.evd f -> clenv.evd, Univ.empty_level_subst + | _ -> Evd.refresh_undefined_universes clenv.evd + let e_give_exact flags h = let { hint_term = c; hint_clnv = clenv } = h in let open Tacmach.New in @@ -150,8 +156,9 @@ let e_give_exact flags h = let sigma = project gl in let c, sigma = if h.hint_poly then - let clenv', subst = Clenv.refresh_undefined_univs clenv in - let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in + (* Should we really refresh all universes when we have the local ones at hand? *) + let evd, subst = refresh_undefined_univs clenv in + let evd = evars_reset_evd ~with_conv_pbs:true sigma evd in let c = Vars.subst_univs_level_constr subst c in c, evd else c, sigma @@ -224,7 +231,7 @@ let unify_resolve_refine flags h diff = let with_prods nprods h f = if get_typeclasses_limit_intros () then Proofview.Goal.enter begin fun gl -> - let { hint_term = c; hint_clnv = clenv; hint_poly = poly } = h in + let { hint_term = c; hint_poly = poly } = h in if poly || Int.equal nprods 0 then f None else let sigma = Tacmach.New.project gl in |