Changed some Qeds to Defined for equality proofs

theories/Data/Eq.v

@@ -16,7 +16,7 @@ Lemma eq_sym_eq
     end val.
 Proof.
   destruct pf. reflexivity.
-Qed.
+Defined.
 
 Lemma match_eq_sym_eq
 : forall T (a b : T) (pf : a = b) F X,
@@ -27,7 +27,7 @@ Lemma match_eq_sym_eq
     end = X.
 Proof.
   destruct pf. reflexivity.
-Qed.
+Defined.
 Hint Rewrite match_eq_sym_eq : eq_rw.
 
 Lemma match_eq_sym_eq'
@@ -39,7 +39,7 @@ Lemma match_eq_sym_eq'
     end = X.
 Proof.
   destruct pf. reflexivity.
-Qed.
+Defined.
 Hint Rewrite match_eq_sym_eq' : eq_rw.
 
 
@@ -54,15 +54,15 @@ Lemma match_eq_match_eq
     end.
 Proof.
   intros. subst. auto.
-Qed.
+Defined.
 
 Lemma eq_sym_eq_trans
 : forall T (a b c : T) (pf : a = b) (pf' : b = c),
     eq_sym (eq_trans pf pf') =
     eq_trans (eq_sym pf') (eq_sym pf).
 Proof.
   clear. destruct pf. destruct pf'. reflexivity.
-Qed.
+Defined.
 
 (** Particular Instances **)
 Lemma eq_Const_eq
@@ -72,7 +72,7 @@ Lemma eq_Const_eq
     end = val.
 Proof.
   destruct pf. reflexivity.
-Qed.
+Defined.
 Hint Rewrite eq_Const_eq : eq_rw.
 
 Lemma eq_Arr_eq
@@ -87,12 +87,12 @@ Lemma eq_Arr_eq
     end.
 Proof.
   destruct pf. reflexivity.
-Qed.
+Defined.
 Hint Rewrite eq_Arr_eq : eq_rw.
 
 Lemma eq_sym_eq_sym : forall (T : Type) (a b : T) (pf : a = b),
                         eq_sym (eq_sym pf) = pf.
-Proof. destruct pf. reflexivity. Qed.
+Proof. destruct pf. reflexivity. Defined.
 Hint Rewrite eq_sym_eq_sym : eq_rw.
 
 Ltac autorewrite_eq_rw :=

theories/Data/Option.v

@@ -158,9 +158,13 @@ Qed.
 *)
 
 Global Instance Injective_Some (T : Type) (a b : T) : Injective (Some a = Some b) :=
-{ result := a = b }.
-abstract (inversion 1; auto).
-Defined.
+{ result := a = b
+; injection := 
+    fun P : Some a = Some b =>
+      match P with 
+      | eq_refl => eq_refl
+      end
+}.
 
 Require ExtLib.Core.EquivDec.
 
@@ -211,6 +215,6 @@ Lemma eq_option_eq
           end.
 Proof.
   destruct pf. destruct val; reflexivity.
-Qed.
+Defined.
 
 Hint Rewrite eq_option_eq : eq_rw.