X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FmetadataQuery.ml;h=6db568cb4ab9ad60516bc30f1a0d366e4e6a7b1f;hb=af805d8cb199ea2c532983e29b064cf9861454f4;hp=4beaab5c1e3d668a6ca10460dd9027fa8b8e3a9c;hpb=4d0ef1046012225b44ee5a1768265c52e534109f;p=helm.git

diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml
index 4beaab5c1..6db568cb4 100644
--- a/helm/software/components/tactics/metadataQuery.ml
+++ b/helm/software/components/tactics/metadataQuery.ml
@@ -171,7 +171,8 @@ let close_with_constructors s metasenv context =
 			     List.fold_left 
 			       (fun (j,s) _ -> 
 				  let curi = UriManager.uri_of_uriref uri i (Some j) in
-                                    prerr_endline ("adding " ^ (UriManager.string_of_uri curi));
+(*                                     prerr_endline ("adding " ^
+ *                                     (UriManager.string_of_uri curi)); *)
 				    j+1,Constr.UriManagerSet.add curi s) (1,s) cl in
 			     (i+1,s)) (0,bag) tl)
 	       | _ -> assert false)
@@ -273,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