[Set Keep Proof Equalities.] should not be needed to make [Scheme Equality] succeed

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#5281
From: @JasonGross
Reported version: 8.6
CC: @herbelin

See also: #5261
See also: #5276
See also: #5277
See also: #5278
See also: #5279
See also: #5280
See also: #5282
See also: #5283
See also: #5284
See also: #5285

[coqbot]

Comment author: @JasonGross

Inductive A (T : Prop) := B (_ : T).
Fail Scheme Equality for A. (* A_beq is defined
The command has indeed failed with message:
Error:
Unexpected error during scheme creation: Error: No information can be deduced 
from this equality
                                         and the injectivity of constructors. 
This may be because
                                         the terms are convertible, or due to 
pattern matching
                                         restrictions in the sort Prop. You can 
try to use option
                                         Set Keep Proof Equalities.
 *)
Set Keep Proof Equalities.
Scheme Equality for A. (* success *)

[coqbot]

Comment author: @herbelin

Note: There was a fix in #420 replaced by #677.

[coqbot]

Comment author: @Zimmi48

BTW Hugo, #677 is awaiting action from your part.