aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/summary.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/summary.ml')
-rw-r--r--library/summary.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/summary.ml b/library/summary.ml
index d1bbf7191..af4deb40f 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -71,7 +71,7 @@ let unfreeze_summaries fs =
with Not_found -> anomaly (str"Undeclared summary "++str ml_modules_summary));
Hashtbl.iter
(fun id decl ->
- if id = ml_modules_summary then () (* already unfreezed *)
+ if String.equal id ml_modules_summary then () (* already unfreezed *)
else
try decl.unfreeze_function (String.Map.find id fs)
with Not_found -> decl.init_function())