diff options
Diffstat (limited to 'common/Linking.v')
| -rw-r--r-- | common/Linking.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/common/Linking.v b/common/Linking.v index 089f4fd2..d23b1028 100644 --- a/common/Linking.v +++ b/common/Linking.v @@ -869,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]. *) |