From 16b8ed513cb4a0e68456fc968a9a0107d02acf5a Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 25 Apr 2017 13:50:54 -0400
Subject: Give andb_prop a simpler proof

No need to use `discriminate`.  This is the hopefully uncontroversial part of https://github.com/coq/coq/pull/401.---
 theories/Init/Datatypes.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 11d80dbc33..41e1fea61d 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -65,7 +65,7 @@ Infix "&&" := andb : bool_scope.
 
 Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true.
 Proof.
-  destruct a; destruct b; intros; split; try (reflexivity || discriminate).
+  destruct a, b; repeat split; assumption.
 Qed.
 Hint Resolve andb_prop: bool.
 
-- 
cgit v1.2.3