diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/equality.mli | 2 | ||||
| -rw-r--r-- | tactics/leminv.ml | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index c442178c1..5ed9ac2ba 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -88,7 +88,7 @@ type freeze_evars_flag = bool (* true = don't instantiate existing evars *) type orientation = bool type conditions = - | Naive (* Only try the first occurence of the lemma (default) *) + | Naive (* Only try the first occurrence of the lemma (default) *) | FirstSolved (* Use the first match whose side-conditions are solved *) | AllMatches (* Rewrite all matches whose side-conditions are solved *) @@ -1577,7 +1577,7 @@ let restrict_to_eq_and_identity eq = (* compatibility *) exception FoundHyp of (Id.t * constr * bool) -(* tests whether hyp [c] is [x = t] or [t = x], [x] not occuring in [t] *) +(* tests whether hyp [c] is [x = t] or [t = x], [x] not occurring in [t] *) let is_eq_x gl x (id,_,c) = try let c = pf_nf_evar gl c in diff --git a/tactics/equality.mli b/tactics/equality.mli index 3e13ee570..840ede7d9 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -23,7 +23,7 @@ type freeze_evars_flag = bool (* true = don't instantiate existing evars *) type orientation = bool type conditions = - | Naive (* Only try the first occurence of the lemma (default) *) + | Naive (* Only try the first occurrence of the lemma (default) *) | FirstSolved (* Use the first match whose side-conditions are solved *) | AllMatches (* Rewrite all matches whose side-conditions are solved *) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index efd6ded44..42d22bc3c 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -124,7 +124,7 @@ let rec add_prods_sign env sigma t = add_prods_sign (push_named (id,Some c1,t1) env) sigma b' | _ -> (env,t) -(* [dep_option] indicates wether the inversion lemma is dependent or not. +(* [dep_option] indicates whether the inversion lemma is dependent or not. If it is dependent and I is of the form (x_bar:T_bar)(I t_bar) then the stated goal will be (x_bar:T_bar)(H:(I t_bar))(P t_bar H) where P:(x_bar:T_bar)(H:(I x_bar))[sort]. diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 6bd65d0a2..081170869 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1386,7 +1386,7 @@ module Strategies = end -(** The strategy for a single rewrite, dealing with occurences. *) +(** The strategy for a single rewrite, dealing with occurrences. *) (** A dummy initial clauseenv to avoid generating initial evars before even finding a first application of the rewriting lemma, in setoid_rewrite |