X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fdeclarative.ml;h=7561281a854ddd5871a32a577e7912a064517abd;hb=7a8f91f8aa2d6ba24bf6b3093866f759ee16e690;hp=ef052cfcbec5e2db9394eb603978d8a3577e792e;hpb=1e06740d20bed28f2e6f0088344065948878a810;p=helm.git

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index ef052cfcb..7561281a8 100644
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/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 ->
@@ -150,7 +150,7 @@ let rewritingstep ~dbd lhs rhs just conclude =
    match just with
       None ->
        Tactics.auto ~dbd
-        ~params:["paramodulation","1"; "timeout","3"]
+        ~params:["paramodulation","1"; "timeout","3"; "library","1"]
     | Some just -> Tactics.apply just
   in
    match lhs with