diff options
Diffstat (limited to 'test-suite/bugs/closed/3922.v')
| -rw-r--r-- | test-suite/bugs/closed/3922.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v index 93208489..5013bc6a 100644 --- a/test-suite/bugs/closed/3922.v +++ b/test-suite/bugs/closed/3922.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Require Import TestSuite.admit. Set Universe Polymorphism. Notation Type0 := Set. @@ -43,7 +44,7 @@ Notation IsHProp := (IsTrunc -1). Monomorphic Axiom dummy_funext_type : Type0. Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. -Inductive Unit : Type1 := +Inductive Unit : Set := tt : Unit. Record TruncType (n : trunc_index) := BuildTruncType { |