diff options
Diffstat (limited to 'test-suite/modules/PO.v')
| -rw-r--r-- | test-suite/modules/PO.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index da098a420..aafbbf2a1 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -52,8 +52,8 @@ Module Check_Pair [X:PO][Y:PO] : PO := (Pair X Y). Module Type Fmono. - Module X:PO. - Module Y:PO. + Declare Module X:PO. + Declare Module Y:PO. Parameter f : X.T -> Y.T. |