| 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)