diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out
index 81981da720..9f4303a399 100644
--- a/test-suite/output/FunExt.out
+++ b/test-suite/output/FunExt.out
@@ -1,18 +1,18 @@
-File "./output/FunExt.v", line 15, characters 5-24:
+File "./output/FunExt.v", line 17, characters 5-24:
 The command has indeed failed with message:
 Tactic failure: Not an extensional equality.
-File "./output/FunExt.v", line 17, characters 5-24:
+File "./output/FunExt.v", line 19, characters 5-24:
 The command has indeed failed with message:
 Tactic failure: Not an extensional equality.
-File "./output/FunExt.v", line 18, characters 5-26:
+File "./output/FunExt.v", line 20, characters 5-26:
 The command has indeed failed with message:
 Tactic failure: Not an extensional equality.
-File "./output/FunExt.v", line 93, characters 9-28:
+File "./output/FunExt.v", line 97, characters 9-28:
 The command has indeed failed with message:
 Tactic failure: Not an extensional equality.
-File "./output/FunExt.v", line 149, characters 9-28:
+File "./output/FunExt.v", line 153, characters 9-28:
 The command has indeed failed with message:
 Tactic failure: Already an intensional equality.
-File "./output/FunExt.v", line 162, characters 9-29:
+File "./output/FunExt.v", line 166, characters 9-29:
 The command has indeed failed with message:
 Hypothesis e depends on the body of H'