index_hint db c a b precedence
;;
+(*
let db () =
let combine f l =
List.flatten
!user_db (List.flatten hints)
*)
;;
+*)
let saturate ?(delta=0) metasenv subst context ty goal_arity =
assert (goal_arity >= 0);
;;
let look_for_hint hdb metasenv subst context t1 t2 =
+ if NDiscriminationTree.NCicIndexable.path_string_of t1 =
+ [Discrimination_tree.Variable] ||
+ NDiscriminationTree.NCicIndexable.path_string_of t2 =
+ [Discrimination_tree.Variable] then [] else begin
+
debug(lazy ("KEY1: "^NCicPp.ppterm ~metasenv ~subst ~context t1));
debug(lazy ("KEY2: "^NCicPp.ppterm ~metasenv ~subst ~context t2));
(*
rc)));
rc
+ end
;;
let pp_hint t p =