summaryrefslogtreecommitdiff
path: root/test-suite/modules/PO.v
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:28 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:28 -0500
commit1ef7f1c0c6897535a86daa77799714e25638f5e9 (patch)
tree5bcca733632ecc84d2c6b1ee48cb2e557a7adba5 /test-suite/modules/PO.v
parent3a2fac7bcee36fd9dcb4f39a615c8ac0349abcc9 (diff)
parent9ebf44d84754adc5b64fcf612c6816c02c80462d (diff)
Updated version 8.9.0 from 'upstream/8.9.0'
Diffstat (limited to 'test-suite/modules/PO.v')
-rw-r--r--test-suite/modules/PO.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
index 8ba8525c..be331049 100644
--- a/test-suite/modules/PO.v
+++ b/test-suite/modules/PO.v
@@ -1,8 +1,8 @@
Set Implicit Arguments.
Unset Strict Implicit.
-Implicit Arguments fst.
-Implicit Arguments snd.
+Arguments fst : default implicits.
+Arguments snd : default implicits.
Module Type PO.
Parameter T : Set.