diff options
Diffstat (limited to 'plugins/extraction/mlutil.ml')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 9b72c3e9f..3f5443e03 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -796,7 +796,7 @@ let branch_as_cst (l,_,c) = When searching for the best factorisation below, we'll try both. *) -(* The following structure allows to record which element occurred +(* The following structure allows recording which element occurred at what position, and then finally return the most frequent element and its positions. *) |