From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 1 Apr 2008 12:40:50 +0000 (+0000)
Subject: added to rewrite a check to effectively do something, and fail if nothing has been... 
X-Git-Tag: make_still_working~5479
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=04858c4692eb584390fb53c7034ed7618431a9c0;p=helm.git

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

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