I corrected a (small) type in the file src/michocoq/syntax.v : changed update_mao to update_map
update_mao
update_map