From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 27 May 2009 06:38:45 +0000 (+0000)
Subject: Avoiding to filter the application of congruence equations
X-Git-Tag: make_still_working~3944
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=82d4772ee9ac860f0a99b774612d2cf19838bb4b;p=helm.git

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 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 =