X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=6b25982d3bb7377b8a0a5019172e5f3f482ce678;hb=ff52cc33b36594d156f8c7d4351ffe0a34730b62;hp=07331220cbdcadee037d4a1459c80eb759970e0b;hpb=87fdda71e8e0dcf886852f70be9a4b3d627b8e9c;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 07331220c..6b25982d3 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -1,4 +1,5 @@
 (* Copyright (C) 2002, HELM Team.
+
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -182,11 +183,17 @@ let only signature context metasenv t =
     in
     let consts = MetadataConstraints.constants_of ty in
     let b = MetadataConstraints.UriManagerSet.subset consts signature in
+(*     if b then (prerr_endline ("keeping " ^ (CicPp.ppterm t)); b)  *)
     if b then b 
     else
       let ty' = unfold context ty in
       let consts' = MetadataConstraints.constants_of ty' in
-      MetadataConstraints.UriManagerSet.subset consts' signature 
+      let b = MetadataConstraints.UriManagerSet.subset consts' signature  in
+(*
+	if not b then prerr_endline ("filtering " ^ (CicPp.ppterm t))
+	else prerr_endline ("keeping " ^ (CicPp.ppterm t)); 
+*)
+      b
   with 
   | CicTypeChecker.TypeCheckerFailure _ -> assert false
   | ProofEngineTypes.Fail _ -> false (* unfold may fail *)
@@ -207,9 +214,11 @@ let retrieve_equations dont_filter signature universe cache context metasenv =
         let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
         let candidates = get_candidates false universe cache fake_eq in
         if dont_filter then candidates
-        else 
-          let candidates = List.filter not_default_eq_term candidates in
-          List.filter (only signature context metasenv) candidates 
+        else let eq_uri = UriManager.uri_of_uriref eq_uri 0 None in
+          (* let candidates = List.filter not_default_eq_term candidates in *)
+          List.filter 
+	    (only (MetadataConstraints.UriManagerSet.add eq_uri signature) 
+	       context metasenv) candidates 
 
 let build_equality bag head args proof newmetas maxmeta = 
   match head with
@@ -275,7 +284,7 @@ let init_cache_and_tables
     (lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt))));
   let cache = cache_add_list cache context (ct@lt) in  
   let equations = 
-    retrieve_equations dont_filter signature universe cache context metasenv 
+    retrieve_equations dont_filter (* true *) signature universe cache context metasenv 
   in
   debug_print 
     (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));