-(* if not (fst (CicReduction.are_convertible *)
-(* ~metasenv context termty ty ugraph)) then ( *)
-(* (\* debug_print (lazy ( *\) *)
-(* (\* Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *\) *)
-(* (\* (CicPp.pp termty names) (CicPp.pp ty names))); *\) *)
-(* find_matches metasenv context ugraph lift_amount term termty tl *)
-(* ) else *)
+ if check && not (fst (CicReduction.are_convertible
+ ~metasenv context termty ty ugraph)) then (
+(* debug_print (lazy ( *)
+(* Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *)
+(* (CicPp.pp termty names) (CicPp.pp ty names))); *)
+ find_matches metasenv context ugraph lift_amount term termty tl
+ ) else