added to rewrite a check to effectively do something, and fail if nothing has been...

diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml
index bd73865af94ffcf050498704a9be1be71543ff23..72a63571cef7221ae211360b5d44f58ba36a2f20 100644 (file)
--- 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