diff options
Diffstat (limited to 'test-suite/bugs/closed/bug_13896.v')
| -rw-r--r-- | test-suite/bugs/closed/bug_13896.v | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_13896.v b/test-suite/bugs/closed/bug_13896.v new file mode 100644 index 0000000000..10f24d8564 --- /dev/null +++ b/test-suite/bugs/closed/bug_13896.v @@ -0,0 +1,24 @@ +Inductive type : Set := + Tptr : type -> type + | Tref : type -> type + | Trv_ref : type -> type + | Tint : type -> type -> type + | Tvoid : type + | Tarray : type -> type -> type + | Tnamed : type -> type + | Tfunction : type -> type -> type -> type + | Tbool : type + | Tmember_pointer : type -> type -> type + | Tfloat : type -> type + | Tqualified : type -> type -> type + | Tnullptr : type + | Tarch : type -> type -> type +. +Definition type_eq_dec : forall (ty1 ty2 : type), { ty1 = ty2 } + { ty1 <> ty2 }. +Proof. fix IHty1 1. decide equality. Defined. + +Goal (if type_eq_dec (Tptr Tvoid) (Tptr Tvoid) then True else False). +Proof. +timeout 1 cbn. +constructor. +Qed. |