Avoid relying on `Add Field` calling `Add Ring`.#81

Open

maximedenes wants to merge 1 commit intocoq-community:masterfrom maximedenes:add-field-no-add-ring

+4

Commits on Jan 31, 2020

Avoid relying on Add Field calling Add Ring.
maximedenes
committed