From 71a810d2c99d13d27aac943771d75460294bf71f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 19 Jul 2006 16:29:06 +0000 Subject: [PATCH] Bug fixed in rewrite in multiple hypothesis and/or conclusion: a lifting was missing, as usual :-) --- helm/software/components/tactics/equalityTactics.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml index 69466c272..1ef330bd2 100644 --- a/helm/software/components/tactics/equalityTactics.ml +++ b/helm/software/components/tactics/equalityTactics.ml @@ -44,14 +44,16 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit (Tacticals.then_ (rewrite_tac ~direction ~pattern:(None,[he],None) equality) - (rewrite_tac ~direction ~pattern:(None,tl,concl_pat) equality) + (rewrite_tac ~direction ~pattern:(None,tl,concl_pat) + (CicSubstitution.lift 1 equality)) ) status | [_] as hyps_pat when concl_pat <> None -> PET.apply_tactic (Tacticals.then_ (rewrite_tac ~direction ~pattern:(None,hyps_pat,None) equality) - (rewrite_tac ~direction ~pattern:(None,[],concl_pat) equality) + (rewrite_tac ~direction ~pattern:(None,[],concl_pat) + (CicSubstitution.lift 1 equality)) ) status | _ -> let arg,dir2,tac,concl_pat,gty = -- 2.39.2