+ universe raw_gty in
+ let local_cands = search_in_th gty cache in
+ let together global local =
+ List.map c_ast
+ (List.filter (only signature context)
+ (NDiscriminationTree.TermSet.elements global)) @
+ List.map t_ast (Ncic_termSet.elements local) in
+ let candidates = together cands local_cands in
+ let smart_candidates =
+ if smart then
+ match raw_gty with
+ | NCic.Appl (hd::tl) ->
+ let weak_gty =
+ NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0)))
+ (List.length tl)) in
+ let more_cands =
+ NDiscriminationTree.DiscriminationTree.retrieve_unifiables
+ universe weak_gty in
+ let smart_cands =
+ NDiscriminationTree.TermSet.diff more_cands cands in
+ let cic_weak_gty = mk_cic_term context weak_gty in
+ let more_local_cands = search_in_th cic_weak_gty cache in
+ let smart_local_cands =
+ Ncic_termSet.diff more_local_cands local_cands in
+ together smart_cands smart_local_cands
+ | _ -> []
+ else []