diff options
| author | Gaëtan Gilbert | 2020-01-17 17:28:50 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-27 13:54:43 +0100 |
| commit | f011a88bd4be4797617741d6829d2530bc29ebdf (patch) | |
| tree | 42baae9f5d4d4e9f27233649e5d4920ada0b0617 /test-suite | |
| parent | 506b35913103c17e4d27663aa0f977452d5815b0 (diff) | |
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.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Scheme.v | 5 |
1 files changed, 5 insertions, 0 deletions
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. |