X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FmetadataQuery.ml;h=6db568cb4ab9ad60516bc30f1a0d366e4e6a7b1f;hb=bca340f9c590e6530f8346fddd61c9fa0ae7f411;hp=f12cd9a19785e288d2a209b7eb713e47cad97ace;hpb=456ea05ac26bf48e4cdc0d745a92de0d14b3ff80;p=helm.git

diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml
index f12cd9a19..6db568cb4 100644
--- a/helm/software/components/tactics/metadataQuery.ml
+++ b/helm/software/components/tactics/metadataQuery.ml
@@ -274,7 +274,9 @@ let signature_of metasenv goal =
   let ty_set = Constr.constants_of ty in
   let hyp_set = signature_of_hypothesis context metasenv in
   let set = Constr.UriManagerSet.union ty_set hyp_set in
-    close_with_constructors (close_with_types set metasenv context)
+    close_with_types
+     (close_with_constructors (close_with_types set metasenv context)
+	metasenv context)
     metasenv context