X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=973cc1d782433a91e3296b9022dc808b433eb1c7;hb=23f2fafa1bd91f271c0b5cf982b1cc59dc74cc35;hp=67c7fb62d88ff289537c3653c64628953cdc3111;hpb=c78edd42f3ebc7c82bb319b876908bf17288ab04;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 67c7fb62d..973cc1d78 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -38,12 +38,14 @@ let ppterm ctx t =
   let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
   CicPp.pp t names
 ;;
+
 let is_propositional context sort = 
   match CicReduction.whd context sort with
   | Cic.Sort Cic.Prop 
   | Cic.Sort (Cic.CProp _) -> true
   | _-> false
 ;;
+
 let is_in_prop context subst metasenv ty =
   let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
   is_propositional context sort
@@ -1035,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")))
@@ -1631,17 +1633,26 @@ let try_candidate dbd
 
 let applicative_case dbd
   tables depth subst fake_proof goalno goalty metasenv context 
-  universe cache flags
+  signature universe cache flags
 = 
-  let goalty_aux = 
+  (* let goalty_aux = 
     match goalty with
     | Cic.Appl (hd::tl) -> 
         Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
     | _ -> goalty
-  in
+  in *)
+  let goalty_aux = goalty in
   let candidates = 
     get_candidates flags.skip_trie_filtering universe cache goalty_aux
   in
+  (* 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 *)
+  let candidates = List.filter (only signature context metasenv) candidates 
+  in
   let tables, elems = 
     List.fold_left 
       (fun (tables,elems) cand ->
@@ -1712,7 +1723,6 @@ let smart_applicative_case dbd
     (lazy ("smart_candidates" ^ " = " ^ 
              (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
   debug_print debug_msg;
-(* we only filter the smart candidates since they could be too many *)
   let candidates = List.filter (only signature context metasenv) candidates in
   let smart_candidates = 
     List.filter (only signature context metasenv) smart_candidates 
@@ -1771,7 +1781,7 @@ let equational_and_applicative_case dbd
       else
         applicative_case dbd
           tables depth s fake_proof goalno 
-            gty m context universe cache flags
+            gty m context signature universe cache flags
     in
       elems@more_elems, tables, cache, flags            
   else
@@ -1782,7 +1792,7 @@ let equational_and_applicative_case dbd
            gty m context signature universe cache flags
       | None -> 
          applicative_case dbd tables depth s fake_proof goalno 
-           gty m context universe cache flags
+           gty m context signature universe cache flags
     in
       elems, tables, cache, flags  
 ;;