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.

1 files changed, 15 insertions, 15 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7b02443cae..b062da23e0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1265,21 +1265,21 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
   let env = eq_clause.env in
   match find_positions env sigma t1 t2 with
-    | Inl _ ->
-	Proofview.tclZERO (Errors.UserError ("Inj",str"Not a projectable equality but a discriminable one."))
-    | Inr [] ->
-	Proofview.tclZERO (Errors.UserError ("Equality.inj",str"Nothing to do, it is an equality between convertible terms."))
-    | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
-        Proofview.tclZERO (Errors.UserError ("Equality.inj" , str"Nothing to inject."))
-    | Inr posns ->
-        Proofview.tclORELSE
-          (inject_if_homogenous_dependent_pair env sigma u)
-          begin function
-            | Not_dep_pair as e |e when Errors.noncritical e ->
-                inject_at_positions env sigma l2r u eq_clause posns
-                  (tac (clenv_value eq_clause))
-            | reraise -> Proofview.tclZERO reraise
-          end
+  | Inl _ ->
+     Proofview.tclZERO (Errors.UserError ("Inj",strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal."))
+  | Inr [] ->
+     Proofview.tclZERO (Errors.UserError ("Equality.inj",strbrk"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 restrictions in the sort Prop."))
+  | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
+     Proofview.tclZERO (Errors.UserError ("Equality.inj" , str"Nothing to inject."))
+  | Inr posns ->
+     Proofview.tclORELSE
+       (inject_if_homogenous_dependent_pair env sigma u)
+       begin function
+         | Not_dep_pair as e |e when Errors.noncritical e ->
+			       inject_at_positions env sigma l2r u eq_clause posns
+						   (tac (clenv_value eq_clause))
+         | reraise -> Proofview.tclZERO reraise
+       end
 
 let postInjEqTac ipats c n =
   match ipats with