From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 13 May 2009 15:19:18 +0000 (+0000)
Subject: The singature of the "by" universe is added to the goal signature
X-Git-Tag: make_still_working~3982
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c78edd42f3ebc7c82bb319b876908bf17288ab04;p=helm.git

The singature of the "by" universe is added to the goal signature
(so univ is never filtered)
---

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index dda3ee933..67c7fb62d 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -2119,6 +2119,18 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa
   let _,metasenv,subst,_,_, _ = proof in
   let _,context,goalty = CicUtil.lookup_meta goal metasenv in
   let signature = MetadataQuery.signature_of metasenv goal in
+  let signature = 
+    List.fold_left 
+      (fun set t ->
+         let ty, _ = 
+	   CicTypeChecker.type_of_aux' metasenv context t 
+	     CicUniv.oblivion_ugraph
+	 in
+	 MetadataConstraints.UriManagerSet.union set 
+	   (MetadataConstraints.constants_of ty)
+       )
+      signature univ
+  in
   let tables,cache =
     if flags.close_more then
       close_more