diff options
| author | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
| commit | d87c4c472478fbcb30de6efabc68473ee36849a1 (patch) | |
| tree | 5b4e1cb66298db57b978374422822ffdf2673100 /library/summary.ml | |
| parent | 850dfbf59f52b0d3dcba237ee2af5ce99fd1bcd2 (diff) | |
| parent | d00472c59d15259b486868c5ccdb50b6e602a548 (diff) | |
Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Diffstat (limited to 'library/summary.ml')
| -rw-r--r-- | library/summary.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/summary.ml b/library/summary.ml index 9b22945919..b68f1fb01b 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -92,7 +92,7 @@ let unfreeze_summaries ?(partial=false) { summaries; ml_module } = | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".") | Some decl -> Option.iter (fun state -> decl.unfreeze_function state) ml_module end; - (** We must be independent on the order of the map! *) + (* We must be independent on the order of the map! *) let ufz name decl = try decl.unfreeze_function String.Map.(find name summaries) with Not_found -> |