Merge PR coq#16212: Fix test suite after parallel merge coq#16130 and c…

…oq#16129 Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
SkySkimmer · Jun 19, 2022 · 83ce48f · 83ce48f
2 parents 055e440 + 8a421bd
commit 83ce48f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
@@ -84,7 +84,7 @@ foo@{uu u v} =
 Type@{u} -> Type@{v} -> Type@{uu}
      : Type@{max(uu+1,u+1,v+1)}
 (* uu u v |=  *)
-foo@{u u IMPORTANT} = 
+foo@{u u IMPORTANT} =
 Type@{u} -> Type@{IMPORTANT} -> Type@{u}
      : Type@{max(u+1,u+1,IMPORTANT+1)}
 (* u u IMPORTANT |=  *)