You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
in math-comp/analysis#383 we could use the new ring of Kazuhiko but I didn't want to add a new depency.
For coq-robot, we actually use the grobner basis computation but maybe with some work this could be also a simpl ring I need to investigate.
There is an instance of nsatz with rcfType in
https://github.com/affeldt-aist/coq-robot/blob/master/ssr_ext.v
Similarly, there is an instance of nsatz with realType in
math-comp/analysis#383
Should the rcfType instance of nsatz move in Analysis too? Or in MathComp? @CohenCyril @thery
The text was updated successfully, but these errors were encountered: