From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 12 Oct 2006 08:06:48 +0000 (+0000)
Subject: Bug fixed: the conversion was done with the wront argument (a sort of typo).
X-Git-Tag: 0.4.95@7852~902
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2632e0520c373f191b81c3975385d77e71314ca7;hp=daa9c2e4caaec2c2c5c262970c936d87332c85d0;p=helm.git

Bug fixed: the conversion was done with the wront argument (a sort of typo).
---

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 ->