aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssrmatching
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssrmatching')
-rw-r--r--plugins/ssrmatching/ssrmatching.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 25975c84e8..6d1d858648 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -143,7 +143,7 @@ val mk_tpattern :
type find_P =
env -> constr -> int -> k:subst -> constr
-(** [conclude ()] asserts that all mentioned ocurrences have been visited.
+(** [conclude ()] asserts that all mentioned occurrences have been visited.
@return the instance of the pattern, the evarmap after the pattern
instantiation, the proof term and the ssrdit stored in the tpattern
@raise UserEerror if too many occurrences were specified *)