diff --git a/Makefile b/Makefile
index 0a09ef7..13938dc 100644
--- a/Makefile
+++ b/Makefile
@@ -3,9 +3,9 @@ MISSING  =								\
 	find . -name '*.v' ! -name Notes.v				\
 		! -name Extract.v					\
 		! -name CpdtTactics.v					\
-                ! -name '*2.v'                                   |	\
-		xargs egrep -i -Hn '(abort|admit|undefined)'     |	\
-		      egrep -v 'Definition undefined'            |	\
+                ! -name '*2.v'                                    |	\
+		xargs egrep -i -Hn '(Fail|abort|admit|undefined)' |	\
+		      egrep -v 'Definition undefined'             |	\
 		      egrep -v '(old|new|research)/'
 
 VFILES = $(wildcard src/*.v)
diff --git a/src/Control/Lens.v b/src/Control/Lens.v
index 2d151da..0a0c9e4 100644
--- a/src/Control/Lens.v
+++ b/src/Control/Lens.v
@@ -8,7 +8,6 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Generalizable All Variables.
 Set Primitive Projections.
-Set Universe Polymorphism.
 Unset Transparent Obligations.
 
 Definition Lens s t a b := forall `{Functor f}, (a -> f b) -> s -> f t.