From 2f56f0fcf21902bb1317f1d6f7ba4b593d712646 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 5 Nov 2015 16:04:43 -0500 Subject: Fix bug #4293: ensure let-ins do not contain algebraic universes in their type annotation. --- test-suite/bugs/closed/4293.v | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 test-suite/bugs/closed/4293.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/4293.v b/test-suite/bugs/closed/4293.v new file mode 100644 index 000000000..3671c931b --- /dev/null +++ b/test-suite/bugs/closed/4293.v @@ -0,0 +1,7 @@ +Module Type Foo. +Definition T := let X := Type in Type. +End Foo. + +Module M : Foo. +Definition T := let X := Type in Type. +End M. \ No newline at end of file -- cgit v1.2.3