From f011a88bd4be4797617741d6829d2530bc29ebdf Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 17 Jan 2020 17:28:50 +0100
Subject: schemes: use rigid universes

so for instance

~~~coq
Set Printing All. Set Printing Universes.

Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= .
Lemma bla@{u v|u < v} : foo@{u v} -> False.
Proof. induction 1. Qed.
~~~

works.
---
 test-suite/success/Scheme.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v
index 855f26698c..4b928007cf 100644
--- a/test-suite/success/Scheme.v
+++ b/test-suite/success/Scheme.v
@@ -25,3 +25,8 @@ Check myeq_rew_fwd_r_dep.
 Set Rewriting Schemes.
 Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true.
 Unset Rewriting Schemes.
+
+(* check that the scheme doesn't minimize itself into something non general *)
+Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= .
+Lemma bla@{u v|u < v} : foo@{u v} -> False.
+Proof. induction 1. Qed.
-- 
cgit v1.2.3