- if flags.local_candidates then
- let mapf s =
- let to_ast = function
- | NCic.Const r when true
- (*is_relevant statistics r*) -> Some (Ast.NRef r)
- (* | NCic.Const _ -> None *)
- | _ -> assert false in
- HExtlib.filter_map
- to_ast (NDiscriminationTree.TermSet.elements s) in
- let g,l =
- get_cands
- (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
- NDiscriminationTree.TermSet.diff
- NDiscriminationTree.TermSet.empty
- raw_gty raw_weak_gty in
- mapf g, mapf l
- else [],[] in
+ let mapf s =
+ let to_ast = function
+ | NCic.Const r when true
+ (*is_relevant statistics r*) -> Some (Ast.NRef r)
+ (* | NCic.Const _ -> None *)
+ | _ -> assert false in
+ HExtlib.filter_map
+ to_ast (NDiscriminationTree.TermSet.elements s) in
+ let g,l =
+ get_cands
+ (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
+ NDiscriminationTree.TermSet.diff
+ NDiscriminationTree.TermSet.empty
+ raw_gty raw_weak_gty in
+ mapf g, mapf l
+ in
+ let global_cands,smart_global_cands =
+ if flags.local_candidates then global_cands,smart_global_cands
+ else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri
+ (NUri.string_of_uri
+ uri) "GLOBAL" | _ -> false)
+ in filter global_cands,filter smart_global_cands
+ in