Avoiding to filter the application of congruence equations

due to a couple of cases in "didactics" where auto is used
instead of reflexivity.

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 34b305ba54d06e7d3f514e9dc2b018bf783805db..973cc1d782433a91e3296b9022dc808b433eb1c7 100644 (file)
--- 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 =