4 files changed, 13 insertions, 13 deletions
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 8f47859da..ef5e18201 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -244,15 +244,16 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite =
        let {Declarations.mind_consnames=consnames ;
             Declarations.mind_typename=typename } = p
        in
-        let arity = Inductive.type_of_inductive (Global.env()) ((mib,p),Univ.Instance.empty)(*FIXME*) in
-        let lc = Inductiveops.arities_of_constructors (Global.env ()) ((sp,!tyno),Univ.Instance.empty)(*FIXME*) in
-        let cons =
+       let inst = Univ.UContext.instance mib.Declarations.mind_universes in
+       let arity = Inductive.type_of_inductive (Global.env()) ((mib,p),inst) in
+       let lc = Inductiveops.arities_of_constructors (Global.env ()) ((sp,!tyno),inst) in
+       let cons =
          (Array.fold_right (fun (name,lc) i -> (name,lc)::i)
-          (Array.mapi
-           (fun j x ->(x,Unshare.unshare lc.(j))) consnames)
-          []
+            (Array.mapi
+               (fun j x ->(x,Unshare.unshare lc.(j))) consnames)
+            []
          )
-        in
+       in
          (typename,finite,Unshare.unshare arity,cons)::i
      ) packs []
    in
diff --git a/test-suite/bugs/opened/HoTT_coq_030.v b/test-suite/bugs/closed/HoTT_coq_030.v
index 934fcd5d8..fa5ee25ca 100644
--- a/test-suite/bugs/opened/HoTT_coq_030.v
+++ b/test-suite/bugs/closed/HoTT_coq_030.v
@@ -47,7 +47,7 @@ Record SpecializedFunctor
     }.
 
 Section Functor.
-  Variable C D : Category.
+  Context (C D : Category).
 
   Definition Functor := SpecializedFunctor C D.
 End Functor.
@@ -235,7 +235,7 @@ Section FullyFaithful.
   Context `(C : @SpecializedCategory objC).
 
   Set Printing Universes.
-  Fail Check InducedHomNaturalTransformation (Yoneda C).
+  Check InducedHomNaturalTransformation (Yoneda C).
   (* Error: Universe inconsistency (cannot enforce Top.865 = Top.851 because
 Top.851 < Top.869 <= Top.864 <= Top.865). *)
 End FullyFaithful.
diff --git a/test-suite/bugs/opened/HoTT_coq_032.v b/test-suite/bugs/closed/HoTT_coq_032.v
index e6ae8a0c4..3f5d7b021 100644
--- a/test-suite/bugs/opened/HoTT_coq_032.v
+++ b/test-suite/bugs/closed/HoTT_coq_032.v
@@ -11,7 +11,7 @@ Delimit Scope functor_scope with functor.
 
 Local Open Scope category_scope.
 
-Fail Record SpecializedCategory (obj : Type) :=
+Record SpecializedCategory (obj : Type) :=
   {
     Object :> _ := obj;
     Morphism : obj -> obj -> Type;
diff --git a/test-suite/bugs/opened/HoTT_coq_027.v b/test-suite/bugs/opened/HoTT_coq_027.v
index e58092eb6..7f283237a 100644
--- a/test-suite/bugs/opened/HoTT_coq_027.v
+++ b/test-suite/bugs/opened/HoTT_coq_027.v
@@ -20,8 +20,8 @@ Identity Coercion FunctorToType_Id : FunctorToType >-> Functor.
 
 Set Printing Universes.
 Definition FunctorTo_Set2Type `(C : @Category objC) (F : FunctorToSet C)
-: FunctorToType C.
-  Fail refine (@Build_Functor _ C _ TypeCat
+: FunctorToType@{Type Type Type Set} C.
+  refine (@Build_Functor _ C _ TypeCat
                          (fun x => F.(ObjectOf) x)
                          (fun s d m => F.(MorphismOf) _ _ m)).
 (* ??? Toplevel input, characters 8-148:
@@ -40,7 +40,6 @@ The term
  "FunctorToType@{Top.100 Top.101 Top.102 Top.103} C"
 (Universe inconsistency: Cannot enforce Set = Top.103)).
  *)
-admit.
 Defined. (* Toplevel input, characters 0-8:
 Error:
 The term