move CPS notations to Util.CPSNotations

3 files changed, 36 insertions, 37 deletions

diff --git a/_CoqProject b/_CoqProject
index 8e6b344c2..8c5b32418 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -235,6 +235,7 @@ src/Util/AdditionChainExponentiation.v
 src/Util/AutoRewrite.v
 src/Util/Bool.v
 src/Util/BoundedWord.v
+src/Util/CPSNotations.v
 src/Util/CPSUtil.v
 src/Util/ChangeInAll.v
 src/Util/Curry.v
diff --git a/src/Util/CPSNotations.v b/src/Util/CPSNotations.v
new file mode 100644
index 000000000..f6fa31f5e
--- /dev/null
+++ b/src/Util/CPSNotations.v
@@ -0,0 +1,34 @@
+Require Import Crypto.Util.Notations.
+
+(** [x <- f ; C] encodes a call to function [f] with [C] as the
+  continuation. In [C], [x] refers to the output of [f]. *)
+
+(* [cpscall] is a marker to get Coq to print code using this notation only when it was actually used *)
+Definition cpscall {R} (f:forall{T}(continuation:R->T),T) {T} (continuation:R->T)
+:= @f T continuation.
+Notation "x' <- v ; C" := (cpscall v (fun x' => C)).
+
+(** A value of type [~>R] accepts a continuation that takes an
+     argument of type [R].  It is meant to be used in [Definition] and
+     such; for example:
+<<
+     Definition add_cps (a b:nat) : ~> nat.
+>>
+     The return type of the continuation is not yet specified; every
+     [~> R] is universally quantified over the possible return types
+     of the continuations that it can be applied to.
+ *)
+Notation "~> R" := (forall {T} (_:R->T), T).
+
+(** The type [A ~> R] contains functions that takes an argument of
+  type [A] and pass a value of type [R] to the continuation. Functions
+  that take multiple arguments can be encoded as [A -> B ~> C] or [A
+  ~> B ~>C] -- the first form requires both arguments to be specified
+  before its output can be CPS-bound, the latter must be bound once it
+  is partially applied to one argument. *)
+Notation "A ~> R" := (A -> ~>R).
+
+(* [cpsreturn] is a marker to get Coq to print loop notations before a [return] *)
+Definition cpsreturn {T} (x:T) := x.
+(** [return x] passes [x] to the continuation implicit in the previous notations. *)
+Notation "'return' x" := (cpsreturn (fun {T} (continuation:_->T) => continuation x)).
\ No newline at end of file
diff --git a/src/Util/Loop.v b/src/Util/Loop.v
index e9d66b647..26341c805 100644
--- a/src/Util/Loop.v
+++ b/src/Util/Loop.v
@@ -3,46 +3,10 @@ Require Import Coq.ZArith.BinInt.
 Require Import Coq.micromega.Lia.
 Require Import Coq.omega.Omega.
 Require Import Crypto.Util.ZUtil.
-Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Notations Crypto.Util.CPSNotations.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 
-(* TODO: move *)
-Module CPSNotations.
-  (** [x <- f ; C] encodes a call to function [f] with [C] as the
-  continuation. In [C], [x] refers to the output of [f]. *)
-
-  (* [cpscall] is a marker to get Coq to print code using this notation only when it was actually used *)
-  Definition cpscall {R} (f:forall{T}(continuation:R->T),T) {T} (continuation:R->T)
-    := @f T continuation.
-  Notation "x' <- v ; C" := (cpscall v (fun x' => C)).
-
-  (** A value of type [~>R] accepts a continuation that takes an
-     argument of type [R].  It is meant to be used in [Definition] and
-     such; for example:
-<<
-     Definition add_cps (a b:nat) : ~> nat.
->>
-     The return type of the continuation is not yet specified; every
-     [~> R] is universally quantified over the possible return types
-     of the continuations that it can be applied to.
-*)
-  Notation "~> R" := (forall {T} (_:R->T), T).
-
-  (** The type [A ~> R] contains functions that takes an argument of
-  type [A] and pass a value of type [R] to the continuation. Functions
-  that take multiple arguments can be encoded as [A -> B ~> C] or [A
-  ~> B ~>C] -- the first form requires both arguments to be specified
-  before its output can be CPS-bound, the latter must be bound once it
-  is partially applied to one argument. *)
-  Notation "A ~> R" := (A -> ~>R).
-
-  (* [cpsreturn] is a marker to get Coq to print loop notations before a [return] *)
-  Definition cpsreturn {T} (x:T) := x.
-  (** [return x] passes [x] to the continuation implicit in the previous notations. *)
-  Notation "'return' x" := (cpsreturn (fun {T} (continuation:_->T) => continuation x)).
-End CPSNotations.
-
 Section with_state.
   Import CPSNotations.
   Context {state : Type}.