PS to commit d7744304f12e08029ea0a0982278297a4bd74d32:

No, the needed change was to functors_transformations.v and
here is the diff:

--- a/functors_transformations.v
+++ b/functors_transformations.v
@@ -423,7 +423,9 @@ Lemma isaprop_full_and_faithful (C D : precategory) (F : functor C D) :
    isaprop (full_and_faithful F).
 Proof.
   apply isofhleveldirprod.
-  repeat (apply impred; intro).
+  apply impred; intro.
+  apply impred; intro.
+  apply impred; intro.
   simpl. repeat (apply impred; intro).
   apply isapropishinh.
   apply isaprop_faithful.