From e759333a8b5c11247c4cc134fdde8c1bd85a6e17 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 11 Sep 2015 18:07:39 +0200 Subject: Universes: enforce Set <= i for all Type occurrences. --- theories/Init/Logic.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Init') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 50f853f0e..375495c88 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -370,7 +370,7 @@ Module EqNotations. End EqNotations. Import EqNotations. - +Set Printing Universes. Lemma rew_opp_r : forall A (P:A->Type) (x y:A) (H:x=y) (a:P y), rew H in rew <- H in a = a. Proof. intros. -- cgit v1.2.3