diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
| commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
| tree | 074182834cb406d1304aec4233718564a9c06ba1 /plugins/funind/glob_termops.mli | |
| parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) | |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'plugins/funind/glob_termops.mli')
| -rw-r--r-- | plugins/funind/glob_termops.mli | 4 |
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. |