Adapt to coq/coq#16920 (and remove uses of deprecated Minus.minus_plus)

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps

MIT License

41 stars 24 forks source link

Closed olaure01 closed 1 year ago

olaure01 commented 1 year ago

Replace all uses of deprecated Minus.minus_plus, Zdiv.div_Zdiv, Zdiv.mod_Zmod (coq/coq#16920).