Library Waterproof.Util.Evars

Require Export Ltac2.Ltac2.

Require Import Waterproof.Waterproof.
Require Import Waterproof.Notations.Common.

Ltac2 @ external refine_goal_with_evar : string -> unit := "rocq-runtime.plugins.coq-waterproof" "refine_goal_with_evar_external".

Ltac2 @ external blank_evars_in_term : constr -> evar list := "rocq-runtime.plugins.coq-waterproof" "blank_evars_in_term_external".

Ltac2 rename_blank_evars_in_term (base_name : string) (x : constr) :=
  let evars := blank_evars_in_term x in
  let m := List.length evars in
  List.iter (fun ev => Control.new_goal ev) (evars);
  Control.focus 2 (Int.add m 1) (fun () =>
    ltac1:(refine (identity_seal _));
    refine_goal_with_evar base_name; Control.shelve()).