From 9b80e3bb62d4e0464856d7fe3e723caa25c05ef0 Mon Sep 17 00:00:00 2001
From: Jared Roesch <roeschinc@gmail.com>
Date: Thu, 23 Feb 2017 01:20:37 -0800
Subject: [PATCH] feat(library/init/meta/vm): add decidable_eq for vm_obj_kind

---
 library/init/meta/vm.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/library/init/meta/vm.lean b/library/init/meta/vm.lean
index 02f428b591..0b7f6135f1 100644
--- a/library/init/meta/vm.lean
+++ b/library/init/meta/vm.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.meta.tactic init.data.option.basic
+import init.meta.mk_dec_eq_instance
 
 meta constant vm_obj : Type
 
@@ -14,6 +15,9 @@ inductive vm_obj_kind
 | environment | tactic_state | format
 | options | other
 
+instance vm_obj_kind_dec_eq : decidable_eq vm_obj_kind :=
+    by tactic.mk_dec_eq_instance
+
 namespace vm_obj
 meta constant kind            : vm_obj → vm_obj_kind
 /- For simple and constructor vm_obj's, it returns the constructor tag/index.