From c78edd42f3ebc7c82bb319b876908bf17288ab04 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 13 May 2009 15:19:18 +0000
Subject: [PATCH] The singature of the "by" universe is added to the goal
 signature (so univ is never filtered)

---
 helm/software/components/tactics/auto.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

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