From effcbf7fab15673f10dfc2d455cb723b29515d5b Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 5 Sep 2016 13:12:17 +0200
Subject: Removed some implict arguments.

Also changed Local Open to Open Local.
---
 lib/Coqlib.v | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'lib/Coqlib.v')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 6fa82492..18d4d7e1 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -1200,7 +1200,7 @@ Proof.
   subst; exists b1; auto.
   exploit IHlist_forall2; eauto. intros (x2 & U & V); exists x2; auto.
 Qed.
-  
+
 Lemma list_forall2_in_right:
   forall x2 l1 l2,
   list_forall2 l1 l2 -> In x2 l2 -> exists x1, In x1 l1 /\ P x1 x2.
@@ -1209,7 +1209,7 @@ Proof.
   subst; exists a1; auto.
   exploit IHlist_forall2; eauto. intros (x1 & U & V); exists x1; auto.
 Qed.
-  
+
 End FORALL2.
 
 Lemma list_forall2_imply:
@@ -1277,11 +1277,9 @@ Qed.
 
 (** * Definitions and theorems over boolean types *)
 
-Definition proj_sumbool (P Q: Prop) (a: {P} + {Q}) : bool :=
+Definition proj_sumbool {P Q: Prop} (a: {P} + {Q}) : bool :=
   if a then true else false.
 
-Implicit Arguments proj_sumbool [P Q].
-
 Coercion proj_sumbool: sumbool >-> bool.
 
 Lemma proj_sumbool_true:
-- 
cgit