diff options
Diffstat (limited to 'theories/Classes/RelationClasses.v')
| -rw-r--r-- | theories/Classes/RelationClasses.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 86a3a88be9..4b97d75cea 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -283,6 +283,7 @@ Local Open Scope list_scope. (** A compact representation of non-dependent arities, with the codomain singled-out. *) (* Note, we do not use [list Type] because it imposes unnecessary universe constraints *) +#[universes(template)] Inductive Tlist : Type := Tnil : Tlist | Tcons : Type -> Tlist -> Tlist. Local Infix "::" := Tcons. |