diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-09-05 13:12:17 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-09-05 13:12:17 +0200 |
commit | effcbf7fab15673f10dfc2d455cb723b29515d5b (patch) | |
tree | f635daff407a4f1b773cda33c4a0399a145ed5ac /cfrontend/SimplExpr.v | |
parent | 64a1e734dfe24194bafd33cff1fbe4d9e1cfdf14 (diff) | |
download | compcert-effcbf7fab15673f10dfc2d455cb723b29515d5b.tar.gz compcert-effcbf7fab15673f10dfc2d455cb723b29515d5b.zip |
Removed some implict arguments.
Also changed Local Open to Open Local.
Diffstat (limited to 'cfrontend/SimplExpr.v')
-rw-r--r-- | cfrontend/SimplExpr.v | 18 |
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. |