improve efficiency of the reduction interpreter of the checker
improve efficiency of the reduction interpreter of coqtop
fix problem with mixed mono/poly inductive definitions