comment search in snippets because it is too slow for jscoq and leave warning in example in ch2.v/ch2.html. Search (odd _). Search eq odd -coprime. should be kind of (* Search (odd _). *) (* Search eq odd -coprime. *)