moved to pkg-ocaml-maint

[helm.git] / components / metadata / metadataConstraints.ml

diff --git a/components/metadata/metadataConstraints.ml b/components/metadata/metadataConstraints.ml
index a4267c5fc6825faa3ccd11da33dc7e8d00a789ce..73f137a432a5ac4bbb2323ebc239d00c1503d221 100644 (file)
--- 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)