blob: 637b77cc58243fa284896f784a29e9e4f917b31e (
plain)
1
2
3
4
5
6
7
8
|
(* Check non-error failure in case of unsupported decidability scheme *)
Local Set Decidable Equality Schemes.
Inductive a := A with b := B.
(* But fails with error if explicitly asked for the scheme *)
Fail Scheme Equality for a.
|
