From efc0f520d536e013740d34e40b298039fca40d19 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 26 May 2010 11:57:37 +0000 Subject: Typo in documentation git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1347 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Coqlib.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/Coqlib.v') diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 380ac738..75e158bd 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. -- cgit