diff options
Diffstat (limited to 'test-suite/output')
-rw-r--r-- | test-suite/output/qualification.out | 3 | ||||
-rw-r--r-- | test-suite/output/qualification.v | 19 |
2 files changed, 0 insertions, 22 deletions
diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out deleted file mode 100644 index 3cf3c2d8f..000000000 --- a/test-suite/output/qualification.out +++ /dev/null @@ -1,3 +0,0 @@ -File "/home/pm/sources/coq/test-suite/output/qualification.v", line 19, characters 0-7: -Error: Signature components for label test do not match: expected type -"Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t". diff --git a/test-suite/output/qualification.v b/test-suite/output/qualification.v deleted file mode 100644 index d39097e2d..000000000 --- a/test-suite/output/qualification.v +++ /dev/null @@ -1,19 +0,0 @@ -Module Type T1. - Parameter t : Type. -End T1. - -Module Type T2. - Declare Module M : T1. - Parameter t : Type. - Parameter test : t = M.t. -End T2. - -Module M1 <: T1. - Definition t : Type := bool. -End M1. - -Module M2 <: T2. - Module M := M1. - Definition t : Type := nat. - Lemma test : t = t. Proof. reflexivity. Qed. -End M2. |