4 files changed, 9 insertions, 35 deletions
diff --git a/test-suite/bugs/closed/3454.v b/test-suite/bugs/closed/3454.v
index 43108ab4b..ca4d23803 100644
--- a/test-suite/bugs/closed/3454.v
+++ b/test-suite/bugs/closed/3454.v
@@ -1,8 +1,11 @@
 Set Primitive Projections.
 Set Implicit Arguments.
+
+Record prod {A} {B}:= pair { fst : A ; snd : B }.
+Notation " A * B " := (@prod A B) : type_scope.
 Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
 Notation pr1 := (@projT1 _ _).
-
+Arguments prod : clear implicits.
 
 Check (@projT1 _ (fun x : nat => x = x)).
 Check (fun s : @sigT nat (fun x : nat => x = x) => s.(projT1)).
@@ -13,7 +16,7 @@ Check (fun r : @rimpl true 0 => r.(foo) (x:=0)).
 Check (fun r : @rimpl true 0 => @foo true 0 r 0).
 Check (fun r : @rimpl true 0 => foo r (x:=0)).
 Check (fun r : @rimpl true 0 => @foo _ _ r 0).
-Check (fun r : @rimpl true 0 => r.(@foo)).
+Check (fun r : @rimpl true 0 => r.(@foo _ _)).
 Check (fun r : @rimpl true 0 => r.(foo)).
 
 Notation "{ x : T  & P }" := (@sigT T P).
diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/closed/HoTT_coq_054.v
index b47bb3a20..c68796593 100644
--- a/test-suite/bugs/closed/HoTT_coq_054.v
+++ b/test-suite/bugs/closed/HoTT_coq_054.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *)
 Inductive Empty : Prop := .
 
 Inductive paths {A : Type} (a : A) : A -> Type :=
@@ -47,10 +47,10 @@ Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
                          | inl y' => ap g
                          | inr y' => idmap
                        end
-           | inr x' => match y as y return match y return Type with
+           | inr x' => match y as y return match y return Prop with
                                                inr y' => x' = y'
                                              | _ => Empty
-                                           end -> match f y return Type with
+                                           end -> match f y return Prop with
                                                     | inr y' => h x' = y'
                                                     | _ => Empty end with
                          | inl y' => idmap
diff --git a/test-suite/bugs/closed/HoTT_coq_108.v b/test-suite/bugs/closed/HoTT_coq_108.v
index 77f921b7c..cc3048027 100644
--- a/test-suite/bugs/closed/HoTT_coq_108.v
+++ b/test-suite/bugs/closed/HoTT_coq_108.v
@@ -115,7 +115,7 @@ Section path_functor.
   Proof.
     intros [H' H''].
     destruct F, G; simpl in *.
-    induction H'; induction H''; simpl.
+    induction H'. (* while destruct H' works *) destruct H''.
     apply ap11; [ apply ap | ];
     apply center; abstract exact _.
     Set Printing Universes.
diff --git a/test-suite/bugs/opened/HoTT_coq_083.v b/test-suite/bugs/opened/HoTT_coq_083.v
deleted file mode 100644
index 091720272..000000000
--- a/test-suite/bugs/opened/HoTT_coq_083.v
+++ /dev/null
@@ -1,29 +0,0 @@
-Set Primitive Projections.
-Set Implicit Arguments.
-Set Universe Polymorphism.
-
-Record category :=
-  { ob : Type }.
-
-Goal forall C, ob C -> ob C.
-intros.
-generalize dependent (ob C).
-(* 1 subgoals, subgoal 1 (ID 7)
-
-  C : category
-  ============================
-   forall T : Type, T -> T
-(dependent evars:) *)
-intros T t.
-Undo 2.
-generalize dependent (@ob C).
-(* 1 subgoals, subgoal 1 (ID 6)
-
-  C : category
-  X : ob C
-  ============================
-   Type -> ob C
-(dependent evars:) *)
-Fail intros T t.
-(* Toplevel input, characters 9-10:
-Error: No product even after head-reduction. *)