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

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