From 2ed097cfba9136a0fba9b961d24c408077fac11d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 13 Feb 2020 16:52:33 +0100
Subject: ComInductive: use lbound=Prop iff non polymorphic

This avoids having to interp params and intern arities twice.
---
 test-suite/output/UnivBinders.out | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 525ca48bee..04514c15cb 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -67,9 +67,9 @@ mono
 The command has indeed failed with message:
 Universe u already exists.
 bobmorane = 
-let tt := Type@{UnivBinders.34} in
-let ff := Type@{UnivBinders.36} in tt -> ff
-     : Type@{max(UnivBinders.33,UnivBinders.35)}
+let tt := Type@{UnivBinders.33} in
+let ff := Type@{UnivBinders.35} in tt -> ff
+     : Type@{max(UnivBinders.32,UnivBinders.34)}
 The command has indeed failed with message:
 Universe u already bound.
 foo@{E M N} = 
@@ -142,16 +142,16 @@ Applied.infunct@{u v} =
 inmod@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
-axfoo@{i UnivBinders.59 UnivBinders.60} :
-Type@{UnivBinders.59} -> Type@{i}
-(* i UnivBinders.59 UnivBinders.60 |=  *)
+axfoo@{i UnivBinders.58 UnivBinders.59} :
+Type@{UnivBinders.58} -> Type@{i}
+(* i UnivBinders.58 UnivBinders.59 |=  *)
 
 axfoo is universe polymorphic
 Arguments axfoo _%type_scope
 Expands to: Constant UnivBinders.axfoo
-axbar@{i UnivBinders.59 UnivBinders.60} :
-Type@{UnivBinders.60} -> Type@{i}
-(* i UnivBinders.59 UnivBinders.60 |=  *)
+axbar@{i UnivBinders.58 UnivBinders.59} :
+Type@{UnivBinders.59} -> Type@{i}
+(* i UnivBinders.58 UnivBinders.59 |=  *)
 
 axbar is universe polymorphic
 Arguments axbar _%type_scope
-- 
cgit v1.2.3