Stopping injection not to work on discriminable atoms (see #4890).

2 files changed, 13 insertions, 9 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index cc7701ad5..18a1f0201 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -736,7 +736,7 @@ let _ =
       optread  = (fun () -> !keep_proof_equalities_for_injection) ;
       optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
 
-let find_positions env sigma t1 t2 =
+let find_positions env sigma ~no_discr t1 t2 =
   let project env sorts posn t1 t2 =
     let ty1 = get_type_of env sigma t1 in
     let s = get_sort_family_of env sigma ty1 in
@@ -767,7 +767,7 @@ let find_positions env sigma t1 t2 =
             List.flatten
 	      (List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn))
 		0 rargs1 rargs2)
-	  else if Sorts.List.mem InType sorts'
+	  else if Sorts.List.mem InType sorts' && not no_discr
           then (* see build_discriminator *)
 	    raise (DiscrFound (List.rev posn,sp1,sp2))
 	  else 
@@ -791,13 +791,14 @@ let find_positions env sigma t1 t2 =
     Inl (path,c1,c2)
 
 let discriminable env sigma t1 t2 =
-  match find_positions env sigma t1 t2 with
+  match find_positions env sigma ~no_discr:false t1 t2 with
     | Inl _ -> true
     | _ -> false
 
 let injectable env sigma t1 t2 =
-    match find_positions env sigma t1 t2 with
-    | Inl _ | Inr [] | Inr [([],_,_)] -> false
+    match find_positions env sigma ~no_discr:true t1 t2 with
+    | Inl _ -> assert false
+    | Inr [] | Inr [([],_,_)] -> false
     | Inr _ -> true
 
 
@@ -1032,7 +1033,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
-    match find_positions env sigma t1 t2 with
+    match find_positions env sigma ~no_discr:false t1 t2 with
     | Inr _ ->
 	tclZEROMSG (str"Not a discriminable equality.")
     | Inl (cpath, (_,dirn), _) ->
@@ -1414,9 +1415,9 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
 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
+  match find_positions env sigma ~no_discr:true t1 t2 with
   | Inl _ ->
-     tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.")
+     assert false
   | Inr [] ->
      let suggestion =
          if !keep_proof_equalities_for_injection then
@@ -1483,7 +1484,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
   Proofview.Goal.enter { enter = begin fun gl ->
     let sigma =  clause.evd in
     let env = Proofview.Goal.env gl in
-      match find_positions env sigma t1 t2 with
+      match find_positions env sigma ~no_discr:false t1 t2 with
       | Inl (cpath, (_,dirn), _) ->
 	  discr_positions env sigma u clause cpath dirn
       | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index d979c580a..b47be3bbc 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -96,7 +96,10 @@ val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic
 val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic
 val rewriteInConcl : bool -> constr -> unit Proofview.tactic
 
+(* Tells if tactic "discriminate" is applicable *)
 val discriminable : env -> evar_map -> constr -> constr -> bool
+
+(* Tells if tactic "injection" is applicable *)
 val injectable : env -> evar_map -> constr -> constr -> bool
 
 (* Subst *)