From 25cc3da212a2c0ac79835e064312079daed4eaed Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 17 May 2008 15:26:44 +0000 Subject: [PATCH] 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). --- helm/software/components/ng_kernel/TEST | 2 ++ .../components/ng_kernel/bug_universi.ma | 21 +++++++++++++++++++ 2 files changed, 23 insertions(+) create mode 100644 helm/software/components/ng_kernel/bug_universi.ma 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. + -- 2.39.2