1 files changed, 36 insertions, 33 deletions

diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index d0c99883..616eed37 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -4,43 +4,46 @@ Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
 Local Open Scope Primitives_scope.
-Module Paper .
+Module Paper.
 
 (** [paper::ref_incr] *)
 Definition ref_incr_fwd_back (x : i32) : result i32 :=
-  x0 <- i32_add x 1 %i32; Return x0 .
+  x0 <- i32_add x 1%i32; Return x0
+.
 
 (** [paper::test_incr] *)
 Definition test_incr_fwd : result unit :=
-  x <- ref_incr_fwd_back (0 %i32);
-  if negb (x s= 1 %i32) then Fail_ Failure else Return tt
-  .
+  x <- ref_incr_fwd_back (0%i32);
+  if negb (x s= 1%i32) then Fail_ Failure else Return tt
+.
 
 (** Unit test for [paper::test_incr] *)
 Check (test_incr_fwd )%return.
 
 (** [paper::choose] *)
 Definition choose_fwd (T : Type) (b : bool) (x : T) (y : T) : result T :=
-  if b then Return x else Return y .
+  if b then Return x else Return y
+.
 
 (** [paper::choose] *)
 Definition choose_back
   (T : Type) (b : bool) (x : T) (y : T) (ret : T) : result (T * T) :=
-  if b then Return (ret, y) else Return (x, ret) .
+  if b then Return (ret, y) else Return (x, ret)
+.
 
 (** [paper::test_choose] *)
 Definition test_choose_fwd : result unit :=
-  z <- choose_fwd i32 true (0 %i32) (0 %i32);
-  z0 <- i32_add z 1 %i32;
-  if negb (z0 s= 1 %i32)
+  z <- choose_fwd i32 true (0%i32) (0%i32);
+  z0 <- i32_add z 1%i32;
+  if negb (z0 s= 1%i32)
   then Fail_ Failure
   else (
-    p <- choose_back i32 true (0 %i32) (0 %i32) z0;
+    p <- choose_back i32 true (0%i32) (0%i32) z0;
     let (x, y) := p in
-    if negb (x s= 1 %i32)
+    if negb (x s= 1%i32)
     then Fail_ Failure
-    else if negb (y s= 0 %i32) then Fail_ Failure else Return tt)
-  .
+    else if negb (y s= 0%i32) then Fail_ Failure else Return tt)
+.
 
 (** Unit test for [paper::test_choose] *)
 Check (test_choose_fwd )%return.
@@ -51,54 +54,54 @@ Inductive List_t (T : Type) :=
 | ListNil : List_t T
 .
 
-Arguments ListCons {T} _ _  .
-Arguments ListNil {T}  .
+Arguments ListCons {T} _ _.
+Arguments ListNil {T}.
 
 (** [paper::list_nth_mut] *)
 Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
   match l with
   | ListCons x tl =>
-    if i s= 0 %u32
+    if i s= 0%u32
     then Return x
-    else (i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t)
+    else (i0 <- u32_sub i 1%u32; t <- list_nth_mut_fwd T tl i0; Return t)
   | ListNil => Fail_ Failure
   end
-  .
+.
 
 (** [paper::list_nth_mut] *)
 Fixpoint list_nth_mut_back
   (T : Type) (l : List_t T) (i : u32) (ret : T) : result (List_t T) :=
   match l with
   | ListCons x tl =>
-    if i s= 0 %u32
+    if i s= 0%u32
     then Return (ListCons ret tl)
     else (
-      i0 <- u32_sub i 1 %u32;
+      i0 <- u32_sub i 1%u32;
       tl0 <- list_nth_mut_back T tl i0 ret;
       Return (ListCons x tl0))
   | ListNil => Fail_ Failure
   end
-  .
+.
 
 (** [paper::sum] *)
 Fixpoint sum_fwd (l : List_t i32) : result i32 :=
   match l with
   | ListCons x tl => i <- sum_fwd tl; i0 <- i32_add x i; Return i0
-  | ListNil => Return (0 %i32)
+  | ListNil => Return (0%i32)
   end
-  .
+.
 
 (** [paper::test_nth] *)
 Definition test_nth_fwd : result unit :=
   let l := ListNil in
-  let l0 := ListCons (3 %i32) l in
-  let l1 := ListCons (2 %i32) l0 in
-  x <- list_nth_mut_fwd i32 (ListCons (1 %i32) l1) (2 %u32);
-  x0 <- i32_add x 1 %i32;
-  l2 <- list_nth_mut_back i32 (ListCons (1 %i32) l1) (2 %u32) x0;
+  let l0 := ListCons (3%i32) l in
+  let l1 := ListCons (2%i32) l0 in
+  x <- list_nth_mut_fwd i32 (ListCons (1%i32) l1) (2%u32);
+  x0 <- i32_add x 1%i32;
+  l2 <- list_nth_mut_back i32 (ListCons (1%i32) l1) (2%u32) x0;
   i <- sum_fwd l2;
-  if negb (i s= 7 %i32) then Fail_ Failure else Return tt
-  .
+  if negb (i s= 7%i32) then Fail_ Failure else Return tt
+.
 
 (** Unit test for [paper::test_nth] *)
 Check (test_nth_fwd )%return.
@@ -107,10 +110,10 @@ Check (test_nth_fwd )%return.
 Definition call_choose_fwd (p : (u32 * u32)) : result u32 :=
   let (px, py) := p in
   pz <- choose_fwd u32 true px py;
-  pz0 <- u32_add pz 1 %u32;
+  pz0 <- u32_add pz 1%u32;
   p0 <- choose_back u32 true px py pz0;
   let (px0, _) := p0 in
   Return px0
-  .
+.
 
 End Paper .