diff options
| author | Guillaume Melquiond | 2015-10-13 18:30:47 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-10-13 18:30:47 +0200 |
| commit | ed95f122f3c68becc09c653471dc2982b346d343 (patch) | |
| tree | 87e323b2d382c285e1eae864338ea397fda0923d /pretyping | |
| parent | 26974a4a2301cc7b1188a3f2f29f3d3368eccc0b (diff) | |
Fix some typos.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 2 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 6 | ||||
| -rw-r--r-- | pretyping/termops.ml | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 8ebb037c24..d3d6901b66 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -525,7 +525,7 @@ let rec check_and_clear_in_constr env evdref err ids c = let clear_hyps_in_evi_main env evdref hyps terms ids = (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some hypothesis does not depend on a element of ids, and erases ids in - the contexts of the evars occuring in evi *) + the contexts of the evars occurring in evi *) let terms = List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in let nhyps = diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 8a5db90590..48911a5a9f 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1011,8 +1011,8 @@ let contextually byhead occs f env sigma t = snd (e_contextually byhead occs f' env sigma t) (* linear bindings (following pretty-printer) of the value of name in c. - * n is the number of the next occurence of name. - * ol is the occurence list to find. *) + * n is the number of the next occurrence of name. + * ol is the occurrence list to find. *) let match_constr_evaluable_ref sigma c evref = match kind_of_term c, evref with @@ -1061,7 +1061,7 @@ let is_projection env = function (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)] * Unfolds the constant name in a term c following a list of occurrences occl. - * at the occurrences of occ_list. If occ_list is empty, unfold all occurences. + * at the occurrences of occ_list. If occ_list is empty, unfold all occurrences. * Performs a betaiota reduction after unfolding. *) let unfoldoccs env sigma (occs,name) c = let unfo nowhere_except_in locs = diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 937471cf76..5a55d47fd1 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -561,7 +561,7 @@ let free_rels m = in frec 1 Int.Set.empty m -(* collects all metavar occurences, in left-to-right order, preserving +(* collects all metavar occurrences, in left-to-right order, preserving * repetitions and all. *) let collect_metas c = |