let _,metasenv,subst,_,_, _ = proof in
let _,context,goalty = CicUtil.lookup_meta goal metasenv in
let signature = MetadataQuery.signature_of metasenv goal in
+ let signature =
+ List.fold_left
+ (fun set t ->
+ let ty, _ =
+ CicTypeChecker.type_of_aux' metasenv context t
+ CicUniv.oblivion_ugraph
+ in
+ MetadataConstraints.UriManagerSet.union set
+ (MetadataConstraints.constants_of ty)
+ )
+ signature univ
+ in
let tables,cache =
if flags.close_more then
close_more