Andrej Dudenhefner

@gares when I try to locally compile `ci-analysis` from coq master, I get error messages such as ``` Warning: Cannot open /home/gares/COQ/master/_build/install/default/lib/coq/theories [cannot-open-path,filesystem] Error: Cannot find a physical path bound...

@silene I cannot create a pull request for the gitlab `flocq` repository. The relevant changes (4 lines changed in `Pff.v`) are https://github.com/mrhaandi/flocq/compare/master...auto-metas. Could you check and, if appropriate, merge them...

The last commit also fixed #16323.

@coqbot ci minimize

> The bench shows a few significant slow downs. Are they worth investigating? I did inspect the percentually biggest slowdowns. They come from the `trivial` tactic being applied to a...

@ppedrot Everything seems to be accounted for. I squashed and rebased on master for the merge.

All of the above test cases succeed, if in auto.ml we set `use_metas_eagerly_in_conv_on_closed_terms = true`, which is also the default option for `simple apply`.

Here is a minimal example, which I will use for regression tests: ```coq Create HintDb db. Parameter P : unit -> unit -> Prop. Axiom HP : forall b, P...

The following `wrap1'`, which is between `wrap1` and `wrap2`, also fails ```coq Inductive wrap1' : unit -> Type := wrap1'I (u : unit) : match u with tt => bool...

Interestingly, for my own lemmas such as ``` Lemma my_in_app_or : forall (A : Type) (l m : list A) (a : A), In a (l ++ m) -> In...