Clean up the `Require Import` lists

math-comp / real-closed

Theorems for Real Closed Fields

13 stars 11 forks source link

Closed pi8027 closed 3 months ago

pi8027 commented 3 months ago

This PR also makes real-closed compatible with math-comp/math-comp#1237.

pi8027 commented 3 months ago

~@proux01 Can you fix Nix CI here too?~ Never mind. I managed to fix it myself.