X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FequalityTactics.ml;h=72a63571cef7221ae211360b5d44f58ba36a2f20;hb=ba5c1c83e77e701ef11625687ec27931bc4bb944;hp=bd73865af94ffcf050498704a9be1be71543ff23;hpb=c6cc2a7227d6750076f591a62d7b1896ebf1ebfa;p=helm.git

diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml
index bd73865af..72a63571c 100644
--- a/helm/software/components/tactics/equalityTactics.ml
+++ b/helm/software/components/tactics/equalityTactics.ml
@@ -174,6 +174,8 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
   let abstr_gty =
    ProofEngineReduction.replace_lifting_csc 0
     ~equality:(==) ~what ~with_what:with_what ~where:lifted_gty in
+  if lifted_gty = abstr_gty then 
+    raise (ProofEngineTypes.Fail (lazy "nothing to do"));
   let abstr_gty = CicMetaSubst.apply_subst subst abstr_gty in
   let pred = C.Lambda (fresh_name, ty, abstr_gty) in
   (* The argument is either a meta if we are rewriting in the conclusion