X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fdeclarative.ml;h=4dcf38b6d56fc6f032fb00bc9aa62481906c6a44;hb=d356a5023cc06477b6d66a7b22a031ad7dffe947;hp=4a7d3e52c6329263d838cf063b6aa9020743d051;hpb=d348c454be6bae89169ed2948067e62e33f62bd8;p=helm.git

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 4a7d3e52c..4dcf38b6d 100644
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -55,8 +55,8 @@ let by_term_we_proved ~dbd t ty id ty' =
    match ty' with
       None -> Tacticals.id_tac
     | Some ty' ->
-       Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
-        (fun _ metasenv ugraph -> ty,metasenv,ugraph)
+        Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+         (fun _ metasenv ugraph -> ty',metasenv,ugraph)
   in
    Tacticals.thens
    ~start: