From 2e8e25217abe62ebf0ed17c3ef6c48f595699433 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 6 Feb 2020 13:29:35 +0100
Subject: Support universe bindings and universe constraints in Let
 definitions.

Let vs Definition / Example syntax was split in 7c28130 for parsing
reasons: so that the new Let Fixpoint and Let CoFixpoint syntax could
be introduced.  This split is probably the reason why Let was
overlooked when support for universe bindings and universe constraints
were added to Definition and variants.
---
 test-suite/success/let_universes.v | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 test-suite/success/let_universes.v

(limited to 'test-suite')

diff --git a/test-suite/success/let_universes.v b/test-suite/success/let_universes.v
new file mode 100644
index 0000000000..c780ec010f
--- /dev/null
+++ b/test-suite/success/let_universes.v
@@ -0,0 +1,5 @@
+Section S.
+Let bla@{} := Prop.
+Let bli@{u} := Type@{u}.
+Fail Let blo@{} := Type.
+End S.
-- 
cgit v1.2.3