From a423d321a98c6f31dab56505fe7acf0110df38e8 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 20 Dec 2005 13:10:03 +0000 Subject: [PATCH] bugfix: typo which implied using the wrong pattern --- helm/ocaml/tactics/equalityTactics.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 0b61e9595..5d995c49b 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -254,7 +254,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = ty_of_with_what ty_of_t_in_context u in if b then let concl_pat_for_t = ProofEngineHelpers.pattern_of ~term:ty [t] in - let pattern_for_t = None,[],concl_pat_for_t in + let pattern_for_t = None,[],Some concl_pat_for_t in t_in_context,pattern_for_t else raise @@ -280,7 +280,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = ~continuations:[ T.then_ ~start:( - rewrite_tac ~direction:`LeftToRight ~pattern (C.Rel 1)) + rewrite_tac ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1)) ~continuation:( T.then_ ~start:( -- 2.39.2