summaryrefslogtreecommitdiff
path: root/plugins/funind/glob_termops.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
commit2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch)
tree074182834cb406d1304aec4233718564a9c06ba1 /plugins/funind/glob_termops.mli
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'plugins/funind/glob_termops.mli')
-rw-r--r--plugins/funind/glob_termops.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 0f10636f..179e8fe8 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -6,7 +6,7 @@ open Misctypes
val get_pattern_id : cases_pattern -> Id.t list
(* [pattern_to_term pat] returns a glob_constr corresponding to [pat].
- [pat] must not contain occurences of anonymous pattern
+ [pat] must not contain occurrences of anonymous pattern
*)
val pattern_to_term : cases_pattern -> glob_constr
@@ -64,7 +64,7 @@ val change_vars : Id.t Id.Map.t -> glob_constr -> glob_constr
(* [alpha_pat avoid pat] rename all the variables present in [pat] s.t.
the result does not share variables with [avoid]. This function create
- a fresh variable for each occurence of the anonymous pattern.
+ a fresh variable for each occurrence of the anonymous pattern.
Also returns a mapping from old variables to new ones and the concatenation of
[avoid] with the variables appearing in the result.