diff options
Diffstat (limited to 'test-suite/bugs/closed/4089.v')
| -rw-r--r-- | test-suite/bugs/closed/4089.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v index 1449f242..e4d76732 100644 --- a/test-suite/bugs/closed/4089.v +++ b/test-suite/bugs/closed/4089.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Require Import TestSuite.admit. (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *) @@ -163,7 +164,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 := |