From e23824e1cc026671c5928000e95c6d6927437b99 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 28 Feb 2019 20:36:00 -0500
Subject: Make [reflect] a typeclass and add a bunch of lemmas

---
 src/Util/Sum.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/Util/Sum.v')

diff --git a/src/Util/Sum.v b/src/Util/Sum.v
index 4d4fde6ac..31019d2da 100644
--- a/src/Util/Sum.v
+++ b/src/Util/Sum.v
@@ -3,6 +3,8 @@ Require Import Coq.Relations.Relation_Definitions.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.GlobalSettings.
 
+Scheme Equality for sum.
+
 Definition sumwise {A B} (RA:relation A) (RB : relation B) : relation (A + B)
   := fun x y => match x, y with
                 | inl x', inl y' => RA x' y'
-- 
cgit v1.2.3