Cyril Cohen

Splitting proofs and reshuffling code

1

##### Motivation for this change This PR slightly refactor the proof of topolology for `\bar R`, for `R : realFieldType` and exhibitting the wrong behaviour for `R : numFieldType`. @affeldt-aist...

##### Motivation for this change @affeldt-aist the counterexample you asked for in https://github.com/math-comp/analysis/pull/1008#issuecomment-1744960401 ##### Things done/to do - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding...

Supporting no purge of algebraic universes

5

CC @gares

Missing API on universes

4

@gares @ecranceMERCE would it make sense to merge this upstream?

A design pattern emerged using HB, ```coq Lemma irrelevant_name one_or_many_params : Mixin one_or_many_params stuff. Proof. blablabla. Qed. HB.instance Definition _ one_or_many_params := irrelevant_name. ``` Sometimes to factor it a bit...

Blacklist internal HB stuff for Search

1

Non exhaustive list of patterns: - ` HB_unamed_mixin` - `__to__` - `__canonical__`

Declarations like ```coq HB.instance Defintiion _ : MyClass _ := MyClass.Build _ ... ``` should be detected and send error message ``` Error: an explicit subject must be provided. ```

The following should succeed but does not ```coq From HB Require Import structures. HB.mixin Record HasPoint T := { default : T }. HB.instance Definition _ A : HasPoint Type...

https://github.com/math-comp/hierarchy-builder/blob/8b1725c9d99e2f0ce6514998b125706aaeb550ac/HB/structure.elpi#L240 Right now we accidentally rely on the fact that simpl will not unfold operators of a structure because it has to go through two delta expansions to see the...

@robbertkrebbers @FissoreD @gares