Removed some implict arguments.

Also changed Local Open to Open Local.

1 files changed, 5 insertions, 13 deletions

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.