diff options
Diffstat (limited to 'test-suite/output/qualification.v')
-rw-r--r-- | test-suite/output/qualification.v | 19 |
1 files changed, 0 insertions, 19 deletions
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. |