Skip to content

Commit

Permalink
Revert "Adapt w.r.t. coq/coq#17768."
Browse files Browse the repository at this point in the history
  • Loading branch information
palmskog committed Aug 8, 2023
1 parent 6ad84f9 commit 323df0a
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/staltac_lib.ml
Original file line number Diff line number Diff line change
Expand Up @@ -262,7 +262,7 @@ let pop_prop_run =
| _ -> get_hyps shyp'
in
let v = get_hyps (pf_hyps_types gl) in
Tacticals.tclTHEN (Generalize.generalize [mkVar v]) (clear [v])
Tacticals.tclTHEN (generalize [mkVar v]) (clear [v])
end

(* Main function *)
Expand Down

0 comments on commit 323df0a

Please sign in to comment.