From 317ae3b327d201530730ed2cce5f44e8763814d4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 17 Oct 2016 17:37:15 +0200 Subject: Removing output test for module qualification. I do not know how to provide a proper test in 8.5, as the location on my machine appears in the error printed when loading the file. Adding a Fail on the End command does not help much either, because it simply does not print anything. Do not merge this commit in 8.6, we still want a test there. --- test-suite/output/qualification.out | 3 --- test-suite/output/qualification.v | 19 ------------------- 2 files changed, 22 deletions(-) delete mode 100644 test-suite/output/qualification.out delete mode 100644 test-suite/output/qualification.v (limited to 'test-suite/output') 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. -- cgit v1.2.3