README: remove ref to closed coq bug

artagnon · Dec 25, 2023 · 1d63c5a · 1d63c5a
1 parent d0d0325
commit 1d63c5a
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/README.md b/README.md
@@ -17,7 +17,6 @@ Our axioms are:
 Section Variables:
 side : HSet
 Axioms:
-STrue relies on definitional UIP. (* bug: coq/coq#16427 *)
 functional_extensionality_dep
   : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
 	(forall x : A, f x = g x) -> f = g