- Fix xml plugin treatment of inductives.

- Move HoTT bug #30 to closed

3 files changed, 5 insertions, 6 deletions

diff --git a/test-suite/bugs/opened/HoTT_coq_030.v b/test-suite/bugs/closed/HoTT_coq_030.v
index 934fcd5d82..fa5ee25cae 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 e6ae8a0c4f..3f5d7b0215 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 e58092eb6f..7f283237a1 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