X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fdeclarative.ml;h=75f56f2b683bdc9f53fe6c5769ec0b7a8dec81cb;hb=7f149c6e78132be469723286161a78a782da70ec;hp=ef052cfcbec5e2db9394eb603978d8a3577e792e;hpb=346c502bf7c78629e75e49f8d9ca379144fdb5df;p=helm.git

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