aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/termops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/termops.ml')
-rw-r--r--engine/termops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/termops.ml b/engine/termops.ml
index 937471cf7..5a55d47fd 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -561,7 +561,7 @@ let free_rels m =
in
frec 1 Int.Set.empty m
-(* collects all metavar occurences, in left-to-right order, preserving
+(* collects all metavar occurrences, in left-to-right order, preserving
* repetitions and all. *)
let collect_metas c =