GitLab

  - many are step limit reached
  - still the typing, and interpretation is done

and use it in Fp theory for defining all formats

  and start adding generic version for interval

  - put extraction in farith2/extracted

Arthur Correnson authored Oct 10, 2021 and François Bobot committed May 27, 2022

+ Add Assert.v module to describe runtime assertions
+ Rename some theorem in Correction_thm.v for better readability
+ Minimal implementation of a GenericFloat module using runtime assertions

update to Coq 8.6 and flocq v4161c990053985f6819e

Feature/rounding

Et voici de beaux rounding modes pour F.
Un peu galère pour trouver des tests où les différents modes d'arrondis sur les _tie breaks_ sont visibles, mais je crois que j'ai trouvé 😅

See merge request !8