aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorThéo Zimmermann2020-05-14 12:50:52 +0200
committerThéo Zimmermann2020-05-14 12:51:07 +0200
commitefa36e61d6eb5421c3c16d66c6d390268892edf2 (patch)
treeb9fce2d32359ed28c074a4ebdb6c40ba93d479ed /plugins
parent26cd7d093822556fc919dc7e27cac0196f564fc2 (diff)
parent6f2b88649ec0c1e27befe7bcd2cdbec0ccee95d6 (diff)
Fix conflicts with latest master.
Diffstat (limited to 'plugins')
-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