Skip to content

Commit

Permalink
Don't nf_univ_variables in prepare_hint
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Oct 26, 2023
1 parent 08dcbc5 commit 908cecc
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion tactics/hints.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1411,7 +1411,6 @@ let prepare_hint env init (sigma,c) =
(* We re-abstract over uninstantiated evars and universes.
It is actually a bit stupid to generalize over evars since the first
thing make_resolves will do is to re-instantiate the products *)
let sigma = Evd.nf_univ_variables sigma in
let c = Evarutil.nf_evar sigma c in
let c = drop_extra_implicit_args sigma c in
let vars = ref (collect_vars sigma c) in
Expand Down

0 comments on commit 908cecc

Please sign in to comment.