Delete reaming About in SplitTypeCat_General

Author: tvignon

TypeTheory/Initiality/SplitTypeCat_General.v

@@ -300,8 +300,7 @@ Section Terms.
     + eapply (map_into_Pb _ _ _ _ _ (reind_pb_typecat A _) _ _ (idpath (identity _ ;; _))).
     + apply Pb_map_commutes_1.
   Defined.
-  About reind_comp_typecat.
-About q_q_typecat.
+
   (* TODO: upstream; consider whether this should be primitive instead of [q_q_typecat]. *)
   Definition q_q_typecat' {C : split_typecat}
     : ∏ Γ (A : C Γ) Γ' (f : Γ' --> Γ) Γ'' (g : Γ'' --> Γ'),