aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/coq_micromega.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/coq_micromega.ml')
-rw-r--r--plugins/micromega/coq_micromega.ml4
1 files changed, 1 insertions, 3 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index ee2c87d19a..0f8d941b41 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1897,8 +1897,6 @@ type provername = string * int option
* The caching mechanism.
*)
-open Persistent_cache
-
module MakeCache (T : sig
type prover_option
type coeff
@@ -1922,7 +1920,7 @@ struct
Hash.((hash_pair T.hash_prover_option (List.fold_left hash_cstr)) 0)
end
- include PHashtable (E)
+ include Persistent_cache.PHashtable (E)
let memo_opt use_cache cache_file f =
let memof = memo cache_file f in