sig val coqtt : Constr.constr end