diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-17 17:37:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-18 10:32:15 +0200 |
| commit | 317ae3b327d201530730ed2cce5f44e8763814d4 (patch) | |
| tree | 76f417fdb434d8b9c149dc2726aa902d6ef3df43 | |
| parent | fa1cb4a55262a1dced369ae6556265b968f4b9a3 (diff) | |
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.
| -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. |