From 94ecebccbab9ceb3c4f9b58eb2d6b3ecd17667d3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 10 Nov 2016 09:51:45 +0100
Subject: [PATCH] Remove Existing Class Is_true.

Having Is_true as a type class caused problems with rewrite: when the
rewrited lemma has a premise of the shape Is_true, the rewrite tactic
will complain that it cannot find a type class instance, instead
of generating a goal for that premise.
---
 theories/base.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 8f01258a..c097a713 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -375,8 +375,6 @@ Notation zip := (zip_with pair).
 Coercion Is_true : bool >-> Sortclass.
 Hint Unfold Is_true.
 Hint Immediate Is_true_eq_left.
-Existing Class Is_true.
-Instance true_Is_true : Is_true true := I.
 Hint Resolve orb_prop_intro andb_prop_intro.
 Notation "(&&)" := andb (only parsing).
 Notation "(||)" := orb (only parsing).
-- 
GitLab