From d82f2c96e73484aae7e6f9e014823065584fbc6e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 26 Feb 2015 09:21:21 +0100 Subject: Moving test for bug #3681 as closed. --- test-suite/bugs/closed/3681.v | 20 ++++++++++++++++++++ test-suite/bugs/opened/3681.v | 20 -------------------- 2 files changed, 20 insertions(+), 20 deletions(-) create mode 100644 test-suite/bugs/closed/3681.v delete mode 100644 test-suite/bugs/opened/3681.v diff --git a/test-suite/bugs/closed/3681.v b/test-suite/bugs/closed/3681.v new file mode 100644 index 0000000000..194113c6ed --- /dev/null +++ b/test-suite/bugs/closed/3681.v @@ -0,0 +1,20 @@ +Module Type FOO. + Parameters P Q : Type -> Type. +End FOO. + +Module Type BAR. + Declare Module Import foo : FOO. + Parameter f : forall A, P A -> Q A -> A. +End BAR. + +Module Type BAZ. + Declare Module Export foo : FOO. + Parameter g : forall A, P A -> Q A -> A. +End BAZ. + +Module BAR_FROM_BAZ (baz : BAZ) : BAR. + Import baz. + Module foo <: FOO := foo. + Import foo. + Definition f : forall A, P A -> Q A -> A := g. +End BAR_FROM_BAZ. diff --git a/test-suite/bugs/opened/3681.v b/test-suite/bugs/opened/3681.v deleted file mode 100644 index 194113c6ed..0000000000 --- a/test-suite/bugs/opened/3681.v +++ /dev/null @@ -1,20 +0,0 @@ -Module Type FOO. - Parameters P Q : Type -> Type. -End FOO. - -Module Type BAR. - Declare Module Import foo : FOO. - Parameter f : forall A, P A -> Q A -> A. -End BAR. - -Module Type BAZ. - Declare Module Export foo : FOO. - Parameter g : forall A, P A -> Q A -> A. -End BAZ. - -Module BAR_FROM_BAZ (baz : BAZ) : BAR. - Import baz. - Module foo <: FOO := foo. - Import foo. - Definition f : forall A, P A -> Q A -> A := g. -End BAR_FROM_BAZ. -- cgit v1.2.3