diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-26 11:57:37 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-26 11:57:37 +0000 |
| commit | efc0f520d536e013740d34e40b298039fca40d19 (patch) | |
| tree | c1e84d3c69ff41d6bf9d80afd61fa23a3dc519b7 /lib | |
| parent | 3a050b22f37f3c79a10a8ebae3d292fa77e91b76 (diff) | |
Typo in documentation
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1347 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Coqlib.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 380ac73..75e158b 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -1104,7 +1104,7 @@ Proof. induction 1; intros. auto. apply IHis_tail. eapply is_tail_cons_left; eauto. Qed. -(** [list_forall2 P [x1 ... xN] [y1 ... yM] holds iff [N = M] and +(** [list_forall2 P [x1 ... xN] [y1 ... yM]] holds iff [N = M] and [P xi yi] holds for all [i]. *) Section FORALL2. |