+ flags status tcache signature gty in
+ (* if the goal is an equation we avoid to apply unit equalities,
+ since superposition should take care of them; refl is an
+ exception since it prompts for convertibility *)
+ let candidates =
+ let test x = not (is_a_fact_ast status subst metasenv context x) in
+ if is_eq then
+ Ast.Ident("refl",None) ::List.filter test candidates
+ else candidates in *)
+ (* new *)
+ let candidates, smart_candidates =
+ get_candidates ~smart:true depth
+ flags status tcache signature gty in
+ (* if the goal is an equation we avoid to apply unit equalities,
+ since superposition should take care of them; refl is an
+ exception since it prompts for convertibility *)
+ let candidates,smart_candidates =
+ let test x = not (is_a_fact_ast status subst metasenv context x) in
+ if is_eq then
+ Ast.Ident("refl",None) ::List.filter test candidates,
+ List.filter test smart_candidates
+ else candidates,smart_candidates in