diff options
Diffstat (limited to 'common/Linking.v')
| -rw-r--r-- | common/Linking.v | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/common/Linking.v b/common/Linking.v index ec828ea4..d23b1028 100644 --- a/common/Linking.v +++ b/common/Linking.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -123,7 +124,7 @@ Defined. Next Obligation. inv H; inv H0; constructor; auto. congruence. - simpl. generalize (init_data_list_size_pos z). xomega. + simpl. generalize (init_data_list_size_pos z). extlia. Defined. Next Obligation. revert H; unfold link_varinit. @@ -868,7 +869,7 @@ Infix ":::" := pass_cons (at level 60, right associativity) : linking_scope. Fixpoint compose_passes (l l': Language) (passes: Passes l l') : Pass l l' := match passes in Passes l l' return Pass l l' with | pass_nil l => pass_identity l - | pass_cons l1 l2 l3 pass1 passes => pass_compose pass1 (compose_passes passes) + | pass_cons pass1 passes => pass_compose pass1 (compose_passes passes) end. (** Some more lemmas about [nlist_forall2]. *) |