hole_reset.diff

diff --git a/src/core/holeId.ml b/src/core/holeId.ml
index c93ee7bb..54d087e1 100644
--- a/src/core/holeId.ml
+++ b/src/core/holeId.ml
@@ -10,6 +10,8 @@ module Make (_ : UNIT) = struct
     let x = !counter in
     incr counter;
     x
+  let reset () =
+    counter := 0
 end
 
 let string_of_hole_id = string_of_int
diff --git a/src/core/holeId.mli b/src/core/holeId.mli
index fb966d0f..ef3b216a 100644
--- a/src/core/holeId.mli
+++ b/src/core/holeId.mli
@@ -18,6 +18,7 @@ val string_of_hole_id : t -> string
 module Make (_ : UNIT) : sig
   (** Generates the next hole ID. *)
   val next : unit -> t
+  val reset : unit -> unit
 end
 
 (** Converts an option type to a name. *)
diff --git a/src/core/holes.ml b/src/core/holes.ml
index 6df4d36e..5fc43053 100644
--- a/src/core/holes.ml
+++ b/src/core/holes.ml
@@ -229,9 +229,14 @@ let add_harpoon_subgoal = DynArray.add harpoon_subgoals
 
 let get_harpoon_subgoals () = DynArray.to_list harpoon_subgoals
 
+(* instantiate a counter for hole IDs;
+   this module is kept private to Holes *)
+module ID = HoleId.Make (Module.Unit)
+
 let clear () =
   Hashtbl.clear holes;
-  DynArray.clear harpoon_subgoals
+  DynArray.clear harpoon_subgoals;
+  ID.reset ()
 
 let list () =
   let f k h l = (k, h) :: l in
@@ -249,10 +254,6 @@ let unsafe_parse_lookup_strategy loc (s : string) : lookup_strategy =
   | Some s -> s
   | None -> throw loc (InvalidHoleIdentifier s)
 
-(* instantiate a counter for hole IDs;
-   this module is kept private to Holes *)
-module ID = HoleId.Make (Module.Unit)
-
 let allocate () = ID.next ()
 let assign id h =
   match Hashtbl.find_opt holes id with