From 821381155ac76a248c6f2d3b8aef03b265af4d6d 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.
---
 prelude/base.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/prelude/base.v b/prelude/base.v
index 8f01258a1..c097a713a 100644
--- a/prelude/base.v
+++ b/prelude/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