diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.mli | 4 | ||||
| -rw-r--r-- | plugins/funind/merge.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index bc7e6f8b0..e7732a503 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -379,7 +379,7 @@ let find_fapp (test:constr -> bool) g : fapp_info list = (** [finduction id filter g] tries to apply functional induction on - an occurence of function [id] in the conclusion of goal [g]. If + an occurrence of function [id] in the conclusion of goal [g]. If [id]=[None] then calls to any function are selected. In any case [heuristic] is used to select the most pertinent occurrence. *) let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list) diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 0f10636f0..179e8fe8d 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. diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 69e055c23..60c58730a 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -902,7 +902,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info = (** [merge id1 id2 args1 args2 id] builds and declares a new inductive type called [id], representing the merged graphs of both graphs - [ind1] and [ind2]. identifiers occuring in both arrays [args1] and + [ind1] and [ind2]. identifiers occurring in both arrays [args1] and [args2] are considered linked (i.e. are the same variable) in the new graph. |