From 2632e0520c373f191b81c3975385d77e71314ca7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 12 Oct 2006 08:06:48 +0000 Subject: [PATCH] Bug fixed: the conversion was done with the wront argument (a sort of typo). --- components/tactics/declarative.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml index ef052cfcb..75f56f2b6 100644 --- a/components/tactics/declarative.ml +++ b/components/tactics/declarative.ml @@ -59,7 +59,7 @@ let by_term_we_proved ~dbd t ty id ty' = Tacticals.then_ ~start:(Tactics.change ~pattern:(ProofEngineTypes.conclusion_pattern None) - (fun _ metasenv ugraph -> ty',metasenv,ugraph)) + (fun _ metasenv ugraph -> ty,metasenv,ugraph)) ~continuation:just ) | Some id -> -- 2.39.2