Remove Universe Polymorphism from Lens.v

jwiegley · Mar 29, 2022 · 08959da · 08959da
1 parent 4950096
commit 08959da
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 4 deletions.
diff --git 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
@@ -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.