test/WildCat/SetoidRewrite: change Abort to Defined

Author: jdchristensen

test/WildCat/SetoidRewrite.v

@@ -54,7 +54,7 @@ Section SetoidRewriteTests.
   Proof.
     intros A ? ? ? a b c eq_ab eq_bc.
     by rewrite eq_ab, <- eq_bc.
-  Abort.
+  Defined.
 
   Goal forall (A : Type) `(H : Is0Gpd A) (a b c : A),
       a $== b -> b $== c -> a $== c.
@@ -64,22 +64,22 @@ Section SetoidRewriteTests.
     rewrite eq_ab, <- eq_bc.
     rewrite eq_bc.
     by rewrite <- eq_bc.
-  Abort.
+  Defined.
 
   Goal forall (A B : Type) (F : A -> B) `{Is1Functor _ _ F} (a b : A) (f g : a $-> b), f $== g -> fmap F f $== fmap F g.
   Proof.
     do 17 intro.
     intro eq_fg.
     by rewrite eq_fg.
-  Abort.
+  Defined.
 
   Goal forall (A : Type) `{Is1Cat A} (a b c : A) (f1 f2 : a $-> b) (g : b $-> c), f1 $== f2 -> g $o f1 $== g $o f2.
   Proof.
     do 11 intro.
     intro eq.
     rewrite <- eq.
     by rewrite eq.
-  Abort.
+  Defined.
 
   Goal forall (A : Type) `{Is1Cat A} (a b c : A) (f : a $-> b) (g1 g2 : b $-> c), g1 $== g2 -> g1 $o f $== g2 $o f.
   Proof.
@@ -88,7 +88,7 @@ Section SetoidRewriteTests.
   rewrite <- eq.
   rewrite eq.
   by rewrite <- eq.
-  Abort.
+  Defined.
 
   Goal forall (A : Type) `{Is1Cat A} (a b c : A) (f1 f2 : a $-> b) (g1 g2 : b $-> c), g1 $== g2 -> f1 $== f2 -> g1 $o f1 $== g2 $o f2.
   Proof.
@@ -98,6 +98,6 @@ Section SetoidRewriteTests.
     rewrite <- eq_f.
     rewrite eq_f.
     by rewrite <- eq_g.
-  Abort.
+  Defined.
 
 End SetoidRewriteTests.