Merge branch 'forhott' into v8.5

3 files changed, 19 insertions, 10 deletions

diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v
index e594b74b62..666c64631f 100644
--- a/test-suite/bugs/closed/3825.v
+++ b/test-suite/bugs/closed/3825.v
@@ -14,3 +14,11 @@ Notation qux := (nat -> nat).
 
 Fail Check qux@{i}.
 
+Axiom TruncType@{i} : nat -> Type@{i}.
+
+Notation "n -Type" := (TruncType n) (at level 1) : type_scope.
+Notation hProp := (0)-Type.
+
+Check hProp.
+Check hProp@{i}.
+
diff --git a/test-suite/bugs/closed/4375.v b/test-suite/bugs/closed/4375.v
index 03af16535b..71e3a75187 100644
--- a/test-suite/bugs/closed/4375.v
+++ b/test-suite/bugs/closed/4375.v
@@ -93,14 +93,15 @@ Polymorphic CoInductive foo@{i} (T : Type@{i}) : Type@{i} :=
 | A : foo T -> foo T.
 
 Polymorphic CoFixpoint cg@{i} (t : Type@{i}) : foo@{i} t :=
-  @A@{i} t (cg@{i} t).
+  @A@{i} t (cg t).
 
 Print cg.
 
 Polymorphic CoFixpoint ca@{i} (t : Type@{i}) : foo@{i} t :=
-  @A@{i} t (@cb@{i} t)
+  @A@{i} t (cb t)
 with cb@{i} (t : Type@{i}) : foo@{i} t :=
-  @A@{i} t (@ca@{i} t).
+  @A@{i} t (ca t).
 
 Print ca.
-Print cb.
\ No newline at end of file
+Print cb.
+  
\ No newline at end of file
diff --git a/test-suite/success/vm_univ_poly.v b/test-suite/success/vm_univ_poly.v
index 58fa39743d..62df96c0b8 100644
--- a/test-suite/success/vm_univ_poly.v
+++ b/test-suite/success/vm_univ_poly.v
@@ -38,8 +38,8 @@ Definition _4 : sumbool_copy x = x :=
 
 (* Polymorphic Inductive Types *)
 Polymorphic Inductive poption@{i} (T : Type@{i}) : Type@{i} :=
-| PSome : T -> poption@{i} T
-| PNone : poption@{i} T.
+| PSome : T -> poption T
+| PNone : poption T.
 
 Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x : T) : T :=
   match p with
@@ -49,7 +49,7 @@ Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x
 
 Polymorphic Inductive plist@{i} (T : Type@{i}) : Type@{i} :=
 | pnil
-| pcons : T -> plist@{i} T -> plist@{i} T.
+| pcons : T -> plist T -> plist T.
 
 Arguments pnil {_}.
 Arguments pcons {_} _ _.
@@ -59,7 +59,7 @@ Polymorphic Definition pmap@{i j}
   fix pmap (ls : plist@{i} T) : plist@{j} U :=
     match ls with
     | @pnil _ => @pnil _
-    | @pcons _ l ls => @pcons@{j} U (f l) (pmap@{i j} ls)
+    | @pcons _ l ls => @pcons@{j} U (f l) (pmap ls)
     end.
 
 Universe Ubool.
@@ -75,7 +75,7 @@ Eval vm_compute in pmap (fun x => x -> Type) (pcons tbool (pcons (plist tbool) p
 
 Polymorphic Inductive Tree@{i} (T : Type@{i}) : Type@{i} :=
 | Empty
-| Branch : plist@{i} (Tree@{i} T) -> Tree@{i} T.
+| Branch : plist@{i} (Tree T) -> Tree T.
 
 Polymorphic Definition pfold@{i u}
             {T : Type@{i}} {U : Type@{u}} (f : T -> U -> U) :=
@@ -111,7 +111,7 @@ Polymorphic Fixpoint repeat@{i} {T : Type@{i}} (n : nat@{i}) (v : T) : plist@{i}
 Polymorphic Fixpoint big_tree@{i} (n : nat@{i}) : Tree@{i} nat@{i} :=
   match n with
   | O => @Empty nat@{i}
-  | S n' => Branch@{i} nat@{i} (repeat@{i} n' (big_tree@{i} n'))
+  | S n' => Branch@{i} nat@{i} (repeat@{i} n' (big_tree n'))
   end.
 
 Eval compute in height (big_tree (S (S (S O)))).