From 55158e2bd190607dbfccc01027c69c660cc82943 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 17 Nov 2005 18:37:38 +0000 Subject: [PATCH] "Parallel" rewriting in a list of hypothesis and in the conclusion is now allowed. --- helm/ocaml/tactics/equalityTactics.ml | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 20dede31e..e519827f2 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -23,8 +23,8 @@ * http://cs.unibo.it/helm/. *) -let rewrite_tac ~direction ~pattern equality = - let rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status +let rec rewrite_tac ~direction ~pattern equality = + let _rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status = let module C = Cic in let module U = UriManager in @@ -37,6 +37,22 @@ let rewrite_tac ~direction ~pattern equality = let proof,goal = status in let curi, metasenv, pbo, pty = proof in let (metano,context,gty) as conjecture = CicUtil.lookup_meta goal metasenv in + match hyps_pat with + he::(_::_ as tl) -> + PET.apply_tactic + (Tacticals.then_ + (rewrite_tac ~direction + ~pattern:(None,[he],Cic.Implicit None) equality) + (rewrite_tac ~direction ~pattern:(None,tl,concl_pat) equality) + ) status + | [_] as hyps_pat when concl_pat <> Cic.Implicit None -> + PET.apply_tactic + (Tacticals.then_ + (rewrite_tac ~direction + ~pattern:(None,hyps_pat,Cic.Implicit None) equality) + (rewrite_tac ~direction ~pattern:(None,[],concl_pat) equality) + ) status + | _ -> let arg,dir2,tac,concl_pat,gty = match hyps_pat with [] -> None,true,PT.exact_tac,concl_pat,gty @@ -73,7 +89,7 @@ let rewrite_tac ~direction ~pattern equality = ProofEngineStructuralRules.clear dummy ]), pat,gty - | _ -> assert false (*CSC: not implemented yet!*) + | _::_ -> assert false in let if_right_to_left do_not_change a b = match direction with @@ -163,7 +179,7 @@ let rewrite_tac ~direction ~pattern equality = in (proof',goals) in - ProofEngineTypes.mk_tactic (rewrite_tac ~direction ~pattern equality) + ProofEngineTypes.mk_tactic (_rewrite_tac ~direction ~pattern equality) let rewrite_simpl_tac ~direction ~pattern equality = -- 2.39.2