merge n (inspect_conclusion n s) (inspect_conclusion n t)
| Cic.Lambda (_, s, t) ->
merge n (inspect_conclusion n s) (inspect_conclusion n t)
- | Cic.LetIn (_, s, t) ->
- merge n (inspect_conclusion n s) (inspect_conclusion n t)
+ | Cic.LetIn (_, s, ty, t) ->
+ merge n (inspect_conclusion n s)
+ (merge n (inspect_conclusion n ty) (inspect_conclusion n t))
| Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
add_root (n-1) u l
| Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
Some uri, SetSet.empty
| Cic.Cast (t, _) -> inspect_term n t
| Cic.Prod (_, _, t) -> inspect_term n t
- | Cic.LetIn (_, _, t) -> inspect_term n t
+ | Cic.LetIn (_, _, _, t) -> inspect_term n t
| Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
let childunion = inspect_children (n-1) l in
Some u, childunion
| 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)
| Cic.Lambda (_, s, t) ->
UriManagerSet.union (signature_concl s) (signature_concl t)
- | Cic.LetIn (_, s, t) ->
- UriManagerSet.union (signature_concl s) (signature_concl t)
+ | Cic.LetIn (_, s, ty, t) ->
+ UriManagerSet.union (signature_concl s)
+ (UriManagerSet.union (signature_concl ty) (signature_concl t))
| Cic.Appl l -> add l
| Cic.MutCase _
| Cic.Fix _
let rec signature_of = function
| Cic.Cast (t, _) -> signature_of t
| Cic.Prod (_, _, t) -> signature_of t
- | Cic.LetIn (_, _, t) -> signature_of t
+ | Cic.LetIn (_, _, _, t) -> signature_of t
| Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
Some (u, []), add l
| Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->