JasonGross/defeined-opaque.diff

## defeined-opaque.diff
diff -r 4eb6407c6ca3 Functor.v
--- a/Functor.v	Fri May 24 20:09:37 2013 -0400
+++ b/Functor.v	Sun Jun 30 04:03:22 2013 -0400
@@ -240,6 +240,23 @@
   Variable G : SpecializedFunctor D E.
   Variable F : SpecializedFunctor C D.

+  Local Notation CObjectOf x := (G (F x)).
+  Local Notation CMorphismOf m := (MorphismOf G (MorphismOf F m)).
+
+  Definition ComposeFunctors_FCompositionOf s d d' (m1 : Morphism C s d) (m2 : Morphism C d d')
+  : CMorphismOf (Compose m2 m1) = Compose (CMorphismOf m2) (CMorphismOf m1).
+    rewrite <- !FCompositionOf.
+    reflexivity.
+  Defined.
+
+  Definition ComposeFunctors_FIdentityOf x
+  : CMorphismOf (Identity x) = Identity _.
+    rewrite <- !FIdentityOf.
+    reflexivity.
+  Defined.
+
+  Global Opaque ComposeFunctors_FCompositionOf ComposeFunctors_FIdentityOf.
+
   Definition ComposeFunctors' : SpecializedFunctor C E
     := Build_SpecializedFunctor C E
                                 (fun c => G (F c))
@@ -275,11 +292,8 @@
     refine (Build_SpecializedFunctor C E
                                      (fun c => G (F c))
                                      (fun _ _ m => G.(MorphismOf) (F.(MorphismOf) m))
-                                     _
-                                     _);
-    abstract (
-        intros; autorewrite with functor; reflexivity
-      ).
+                                     ComposeFunctors_FCompositionOf
+                                     ComposeFunctors_FIdentityOf).
   Defined.
 End FunctorComposition.
	diff -r 4eb6407c6ca3 Functor.v
	--- a/Functor.v Fri May 24 20:09:37 2013 -0400
	+++ b/Functor.v Sun Jun 30 04:03:22 2013 -0400
	@@ -240,6 +240,23 @@
	Variable G : SpecializedFunctor D E.
	Variable F : SpecializedFunctor C D.

	+ Local Notation CObjectOf x := (G (F x)).
	+ Local Notation CMorphismOf m := (MorphismOf G (MorphismOf F m)).
	+
	+ Definition ComposeFunctors_FCompositionOf s d d' (m1 : Morphism C s d) (m2 : Morphism C d d')
	+ : CMorphismOf (Compose m2 m1) = Compose (CMorphismOf m2) (CMorphismOf m1).
	+ rewrite <- !FCompositionOf.
	+ reflexivity.
	+ Defined.
	+
	+ Definition ComposeFunctors_FIdentityOf x
	+ : CMorphismOf (Identity x) = Identity _.
	+ rewrite <- !FIdentityOf.
	+ reflexivity.
	+ Defined.
	+
	+ Global Opaque ComposeFunctors_FCompositionOf ComposeFunctors_FIdentityOf.
	+
	Definition ComposeFunctors' : SpecializedFunctor C E
	:= Build_SpecializedFunctor C E
	(fun c => G (F c))
	@@ -275,11 +292,8 @@
	refine (Build_SpecializedFunctor C E
	(fun c => G (F c))
	(fun _ _ m => G.(MorphismOf) (F.(MorphismOf) m))
	- _
	- _);
	- abstract (
	- intros; autorewrite with functor; reflexivity
	- ).
	+ ComposeFunctors_FCompositionOf
	+ ComposeFunctors_FIdentityOf).
	Defined.
	End FunctorComposition.