X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=973cc1d782433a91e3296b9022dc808b433eb1c7;hb=235d5cc96af46d0406bdd28222f56b3ee2bf827e;hp=34b305ba54d06e7d3f514e9dc2b018bf783805db;hpb=c71c1ae7fec17ba9e36b7a8fa2ca3bf2c8dfc3b8;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 34b305ba5..973cc1d78 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -1037,7 +1037,7 @@ let apply_smart_aux
         in
         match
           Saturation.solve_narrowing bag (proof'''',newmeta) active passive 
-            1 (*0 infinity*)
+            2 (*0 infinity*)
         with 
           | None, active, passive, bag -> 
               raise (ProofEngineTypes.Fail (lazy ("paramod fails")))
@@ -1645,12 +1645,12 @@ let applicative_case dbd
   let candidates = 
     get_candidates flags.skip_trie_filtering universe cache goalty_aux
   in
-  (* if the goal is an equality we skip the congruence theorems *)
+  (* if the goal is an equality we skip the congruence theorems 
   let candidates =
     if is_equational_case goalty flags 
-    then List.filter not_default_eq_term candidates
-    else candidates
-  in
+    then List.filter not_default_eq_term candidates 
+    else candidates 
+  in *)
   let candidates = List.filter (only signature context metasenv) candidates 
   in
   let tables, elems =