From 04858c4692eb584390fb53c7034ed7618431a9c0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 1 Apr 2008 12:40:50 +0000 Subject: [PATCH] added to rewrite a check to effectively do something, and fail if nothing has been rewritten. --- helm/software/components/tactics/equalityTactics.ml | 2 ++ 1 file changed, 2 insertions(+) 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 -- 2.39.2