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.
---
 backend/RTLgen.v      | 21 ++++++---------------
 cfrontend/SimplExpr.v | 18 +++++-------------
 lib/Coqlib.v          |  8 +++-----
 3 files changed, 14 insertions(+), 33 deletions(-)

diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 49d79fb2..11da630b 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -23,7 +23,7 @@ Require Import Registers.
 Require Import CminorSel.
 Require Import RTL.
 
-Open Local Scope string_scope.
+Local Open Scope string_scope.
 
 (** * Translation environments and state *)
 
@@ -112,16 +112,13 @@ Implicit Arguments Error [A s].
 
 Definition mon (A: Type) : Type := forall (s: state), res A s.
 
-Definition ret (A: Type) (x: A) : mon A :=
+Definition ret {A: Type} (x: A) : mon A :=
   fun (s: state) => OK x s (state_incr_refl s).
 
-Implicit Arguments ret [A].
 
-Definition error (A: Type) (msg: Errors.errmsg) : mon A := fun (s: state) => Error msg.
+Definition error {A: Type} (msg: Errors.errmsg) : mon A := fun (s: state) => Error msg.
 
-Implicit Arguments error [A].
-
-Definition bind (A B: Type) (f: mon A) (g: A -> mon B) : mon B :=
+Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B :=
   fun (s: state) =>
     match f s with
     | Error msg => Error msg
@@ -132,27 +129,21 @@ Definition bind (A B: Type) (f: mon A) (g: A -> mon B) : mon B :=
         end
     end.
 
-Implicit Arguments bind [A B].
-
-Definition bind2 (A B C: Type) (f: mon (A * B)) (g: A -> B -> mon C) : mon C :=
+Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C :=
   bind f (fun xy => g (fst xy) (snd xy)).
 
-Implicit Arguments bind2 [A B C].
-
 Notation "'do' X <- A ; B" := (bind A (fun X => B))
    (at level 200, X ident, A at level 100, B at level 200).
 Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
    (at level 200, X ident, Y ident, A at level 100, B at level 200).
 
-Definition handle_error (A: Type) (f g: mon A) : mon A :=
+Definition handle_error {A: Type} (f g: mon A) : mon A :=
   fun (s: state) =>
     match f s with
     | OK a s' i => OK a s' i
     | Error _ => g s
     end.
 
-Implicit Arguments handle_error [A].
-
 (** ** Operations on state *)
 
 (** The initial state (empty CFG). *)
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index bfdd8ab9..71b67f67 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -25,7 +25,7 @@ Require Import Cop.
 Require Import Csyntax.
 Require Import Clight.
 
-Open Local Scope string_scope.
+Local Open Scope string_scope.
 
 (** State and error monad for generating fresh identifiers. *)
 
@@ -43,17 +43,13 @@ Implicit Arguments Res [A g].
 
 Definition mon (A: Type) := forall (g: generator), result A g.
 
-Definition ret (A: Type) (x: A) : mon A :=
+Definition ret {A: Type} (x: A) : mon A :=
   fun g => Res x g (Ple_refl (gen_next g)).
 
-Implicit Arguments ret [A].
-
-Definition error (A: Type) (msg: Errors.errmsg) : mon A :=
+Definition error {A: Type} (msg: Errors.errmsg) : mon A :=
   fun g => Err msg.
 
-Implicit Arguments error [A].
-
-Definition bind (A B: Type) (x: mon A) (f: A -> mon B) : mon B :=
+Definition bind {A B: Type} (x: mon A) (f: A -> mon B) : mon B :=
   fun g =>
     match x g with
       | Err msg => Err msg
@@ -64,13 +60,9 @@ Definition bind (A B: Type) (x: mon A) (f: A -> mon B) : mon B :=
       end
     end.
 
-Implicit Arguments bind [A B].
-
-Definition bind2 (A B C: Type) (x: mon (A * B)) (f: A -> B -> mon C) : mon C :=
+Definition bind2 {A B C: Type} (x: mon (A * B)) (f: A -> B -> mon C) : mon C :=
   bind x (fun p => f (fst p) (snd p)).
 
-Implicit Arguments bind2 [A B C].
-
 Notation "'do' X <- A ; B" := (bind A (fun X => B))
    (at level 200, X ident, A at level 100, B at level 200)
    : gensym_monad_scope.
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