aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Warnings.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/Warnings.v')
-rw-r--r--test-suite/output/Warnings.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v
index 7465442cab..ce92bcbbb2 100644
--- a/test-suite/output/Warnings.v
+++ b/test-suite/output/Warnings.v
@@ -1,5 +1,5 @@
(* Term in warning was not printed in the right environment at some time *)
-Record A := { B:Type; b:B->B }.
-Definition a B := {| B:=B; b:=fun x => x |}.
+Record A := { B:Type; b:Prop }.
+Definition a B := {| B:=B; b:=forall x, x > 0 |}.
Canonical Structure a.