diff options
| author |  Jason Gross <jgross@mit.edu> | 2014-08-12 11:14:04 -0400 |
|---|---|---|
| committer |  Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr> | 2014-08-25 15:22:40 +0200 |
| commit | 4fef230a1ee1964712e3ac7f325ce00968ac4769 (patch) | |
| tree | 7be49300bc9c989a4ec716685356cb8f5aab752e /theories/MSets | |
| parent | 876b1b39a0304c93c2511ca8dd34353413e91c9d (diff) | |
"allows to", like "allowing to", is improper
It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
Diffstat (limited to 'theories/MSets')
| -rw-r--r-- | theories/MSets/MSetAVL.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index 25d899029..e1fc454ae 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -312,7 +312,7 @@ Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans. Local Hint Resolve elements_spec2. (* Sometimes functional induction will expose too much of - a tree structure. The following tactic allows to factor back + a tree structure. The following tactic allows factoring back a Node whose internal parts occurs nowhere else. *) (* TODO: why Ltac instead of Tactic Notation don't work ? why clear ? *) |