diff options
Diffstat (limited to 'common/Linking.v')
| -rw-r--r-- | common/Linking.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/common/Linking.v b/common/Linking.v index 4ef83d42..54d1628e 100644 --- a/common/Linking.v +++ b/common/Linking.v @@ -862,6 +862,8 @@ Inductive Passes: Language -> Language -> Type := | pass_nil: forall l, Passes l l | pass_cons: forall l1 l2 l3, Pass l1 l2 -> Passes l2 l3 -> Passes l1 l3. +Declare Scope linking_scope. + Infix ":::" := pass_cons (at level 60, right associativity) : linking_scope. (** The pass corresponding to the composition of a list of passes. *) |