test-suite/bugs/closed/3736.v


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.