From: Claudio Sacerdoti Coen Date: Sat, 17 May 2008 15:26:44 +0000 (+0000) Subject: The file bug_universi.ma shows a strage case where the ranked universe X-Git-Tag: make_still_working~5181 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=25cc3da212a2c0ac79835e064312079daed4eaed;p=helm.git The file bug_universi.ma shows a strage case where the ranked universe graph does not contain any universe for one object that does contain a user-provided universe. In turns, this make check.ml fail (since no constraint is defined between Type0, which occurs in the object, and Type1). --- diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST index cefa80913..63db76ef4 100644 --- a/helm/software/components/ng_kernel/TEST +++ b/helm/software/components/ng_kernel/TEST @@ -23,6 +23,8 @@ Utrecht 0.82 0.92 ++++++++++++++++ +file bug_universi.ma: sbaglia a fare il ranking! + [CoRN: calcolo grafi da caricare troppo lento] [Coq: calcolo grafi da caricare troppo lento] [Sophia-Antipolis: calcolo grafi da caricare troppo lento] diff --git a/helm/software/components/ng_kernel/bug_universi.ma b/helm/software/components/ng_kernel/bug_universi.ma new file mode 100644 index 000000000..5711cfb8f --- /dev/null +++ b/helm/software/components/ng_kernel/bug_universi.ma @@ -0,0 +1,21 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +definition Type3 := Type. +definition Type2 : Type3 := Type. +definition Type1 : Type2 := Type. + +inductive t: Type2 ≝ + k: Type3 -> t. +