Trying to improve the error messages of injection.

Below are a few examples where the previous messages were misleading:

Module InProp.

Inductive tree : Prop := Leaf | Node : tree -> tree -> tree.

Variables x y : tree.

(* Wrong msg: "Nothing to do, it is an equality between convertible terms." *)
(* These terms are not convertible *)
Goal Node Leaf Leaf = Leaf -> False.
Fail intros H; injection H.
Abort.

End InProp.

Module InSet.

Inductive tree : Set := Leaf | Node : tree -> tree -> tree.

Variables x y : tree.

(* Wrong msg: "Not a projectable equality but a discriminable one." *)
(* This equality is both projectable and discriminable *)
Goal Node x (Node Leaf Leaf) = Node Leaf Leaf -> False.
intros H.
Fail injection H.
Abort.

End InSet.

0 files changed, 0 insertions, 0 deletions