X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fmetadata%2FmetadataConstraints.ml;h=73f137a432a5ac4bbb2323ebc239d00c1503d221;hb=8e7751f97e50bdc18537aac7478d0621d45ab956;hp=a4267c5fc6825faa3ccd11da33dc7e8d00a789ce;hpb=fbfc3e402894a89b22f57e12b53e090f843a690a;p=helm.git

diff --git a/components/metadata/metadataConstraints.ml b/components/metadata/metadataConstraints.ml
index a4267c5fc..73f137a43 100644
--- a/components/metadata/metadataConstraints.ml
+++ b/components/metadata/metadataConstraints.ml
@@ -377,11 +377,20 @@ and signature_concl =
     | Cic.Const (u,exp_named_subst) -> 
         UriManagerSet.singleton u
     | Cic.MutInd (u, t, exp_named_subst) -> 
+        let rec projections_of uris =
+          List.flatten
+           (List.map 
+            (fun uri ->
+              let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+              projections_of (CicUtil.projections_of_record o uri))
+            uris)
+        in
         let uri = UriManager.uri_of_uriref u t None in
-	UriManagerSet.singleton uri
+        List.fold_right UriManagerSet.add
+          (projections_of [u]) (UriManagerSet.singleton uri)
     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
         let uri = UriManager.uri_of_uriref u t (Some c) in
-	UriManagerSet.singleton uri
+        UriManagerSet.singleton uri
     | Cic.Cast (t, _) -> signature_concl t
     | Cic.Prod (_, s, t) -> 
 	UriManagerSet.union (signature_concl s) (signature_concl t)