diff options
Diffstat (limited to 'test-suite/bugs/closed/4089.v')
| -rw-r--r-- | test-suite/bugs/closed/4089.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v index 1449f242b4..c6cb9c35e6 100644 --- a/test-suite/bugs/closed/4089.v +++ b/test-suite/bugs/closed/4089.v @@ -163,7 +163,7 @@ Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope. Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope. -Inductive Unit : Type1 := +Inductive Unit : Set := tt : Unit. Ltac done := |