From 4f715f056a11046ade48931f94252ceb3b795c4c Mon Sep 17 00:00:00 2001
From: jesper-bengtson <jebe@itu.dk>
Date: Thu, 14 Apr 2016 12:19:28 +0200
Subject: [PATCH] Changed some Qeds to Defined for equality proofs

---
 theories/Data/Eq.v     | 16 ++++++++--------
 theories/Data/Option.v | 12 ++++++++----
 2 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/theories/Data/Eq.v b/theories/Data/Eq.v
index 348e9758..2dae4fe3 100644
--- a/theories/Data/Eq.v
+++ b/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,7 +54,7 @@ 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),
@@ -62,7 +62,7 @@ Lemma eq_sym_eq_trans
     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 :=
diff --git a/theories/Data/Option.v b/theories/Data/Option.v
index 50f37970..6ec36a0f 100644
--- a/theories/Data/Option.v
+++ b/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.