Switch to strict bulleting everywhere

Solve #82 (closed).

The flag isn't enforced anywhere, but with this we can add it seamlessly (ideally soon after so there aren't more violations that creep in).

theories/base.v

@@ -258,7 +258,7 @@ Hint Mode LeibnizEquiv ! - : typeclass_instances.
 
 Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (≡@{A})} (x y : A) :
   x ≡ y ↔ x = y.
-Proof. split; [apply leibniz_equiv | intros ->; reflexivity]. Qed.
+Proof. split; [apply leibniz_equiv|]. intros ->; reflexivity. Qed.
 
 Ltac fold_leibniz := repeat
   match goal with