+ (match metasenv with
+ None ->
+ "?" ^ (string_of_int n) ^ "[" ^
+ String.concat " ; "
+ (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
+ "]"
+ | Some metasenv ->
+ try
+ let _,context,_ = CicUtil.lookup_meta n metasenv in
+ "?" ^ (string_of_int n) ^ "[" ^
+ String.concat " ; "
+ (List.rev
+ (List.map2
+ (fun x y ->
+ match x,y with
+ _, None
+ | None, _ -> "_"
+ | Some _, Some t -> pp t l
+ ) context l1)) ^
+ "]"
+ with
+ CicUtil.Meta_not_found _
+ | Invalid_argument _ ->
+ "???" ^ (string_of_int n) ^ "[" ^
+ String.concat " ; "
+ (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
+ "]"
+ )