aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/rewrite.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/rewrite.ml')
-rw-r--r--tactics/rewrite.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 6bd65d0a2..081170869 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1386,7 +1386,7 @@ module Strategies =
end
-(** The strategy for a single rewrite, dealing with occurences. *)
+(** The strategy for a single rewrite, dealing with occurrences. *)
(** A dummy initial clauseenv to avoid generating initial evars before
even finding a first application of the rewriting lemma, in setoid_rewrite