search

math-comp / analysis

Mathematical Components compliant Analysis Library
Other
205 stars 45 forks source link

Which bigenough? #104

Closed affeldt-aist closed 6 years ago

affeldt-aist commented 6 years ago

This is a minor issue but with "From mathcomp Require Import bigenough" Coq might load the bigenough from real-closed if it is installed. Of course this is ok as long as both are in sync and real-closed properly updated but what about "Require Import mathcomp.bigenough.bigenough"?

https://github.com/math-comp/analysis/blob/3643e6eb0de79a7aefd0282bbf7f3290dc403a20/altreals/realseq.v#L7

CohenCyril commented 6 years ago

Hum, right... this is annoying indeed. Let us take the solution you suggest for now...