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 dda3ee9332755332862ec844f7154fba7e8666b4..67c7fb62d88ff289537c3653c64628953cdc3111 100644 (file)
--- 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