]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed: the conversion was done with the wront argument (a sort of typo).
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 12 Oct 2006 08:06:48 +0000 (08:06 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 12 Oct 2006 08:06:48 +0000 (08:06 +0000)
components/tactics/declarative.ml

index ef052cfcbec5e2db9394eb603978d8a3577e792e..75f56f2b683bdc9f53fe6c5769ec0b7a8dec81cb 100644 (file)
@@ -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 ->