1 (* type naif_indexing =
2 (Cic.term * ((bool * Inference.equality) list)) list
5 type pos = Left | Right
10 | Cic.Appl hd::tl -> hd
15 let (_,(_,l,r,ordering),_,_) = eq in
16 let hl = head_of_term l in
17 let hr = head_of_term r in
20 try Hashtbl.find table x
21 with Not_found -> [] in
22 Hashtbl.replace table x (pos,eq)::x_entry in
33 let demodulate_term env table cmp term =
34 let hd_term = head_of_term term in
35 let candidates = Hashtbl.find table hd_term in