aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/common.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/common.ml')
-rw-r--r--plugins/extraction/common.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 0f0b902c3..6af939c19 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -199,7 +199,7 @@ let empty_env () = [], get_global_ids ()
let mktable autoclean =
let h = Hashtbl.create 97 in
if autoclean then register_cleanup (fun () -> Hashtbl.clear h);
- (Hashtbl.add h, Hashtbl.find h, fun () -> Hashtbl.clear h)
+ (Hashtbl.replace h, Hashtbl.find h, fun () -> Hashtbl.clear h)
(* We might have built [global_reference] whose canonical part is
inaccurate. We must hence compare only the user part,