From c4d7fede86d052f1ffc824eb9a4aa7e3fdb63ea0 Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 7 Mar 2002 10:57:37 +0000
Subject: Simplify_eq echouait sur des hypotheses trivial comme O=O

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2518 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index de98abd610..e1d2821382 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -890,9 +890,8 @@ let decompEqThen ntac id gls =
 	   ((tclTHENS (cut_intro absurd_term)
 	       ([onLastHyp gen_absurdity;
 		 refine (mkApp (pf, [| mkVar id |]))]))) gls
-     | Inr [] ->
-	 errorlabstrm "Equality.inj" 
-	   (str"Nothing to do, it is an equality between convertible terms")
+     | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
+         tclIDTAC gls
      | Inr posns ->
 	 (let e = pf_get_new_id (id_of_string "e") gls in
 	  let e_env = push_named (e,None,t) env in
-- 
cgit v1.2.3