Fix for 8.7

`2: {` is not valid in 8.7

1 files changed, 6 insertions, 6 deletions

diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Experiments/NewPipeline/Toplevel2.v
index cec9fcfb1..81c94b1bc 100644
--- a/src/Experiments/NewPipeline/Toplevel2.v
+++ b/src/Experiments/NewPipeline/Toplevel2.v
@@ -1790,9 +1790,9 @@ Module Fancy.
           cbn. rewrite IHe by auto.
           rewrite Tuple.map_map.
           (*
-           Need to prove that contexts are equivalent and swapping contexts is OK 
+           Need to prove that contexts are equivalent and swapping contexts is OK
           *)
-        (* 
+        (*
              TODO : either prove this lemma or devise a good way to
              prove case-by-case that the output of allocate is
              equivalent to the input.
@@ -2679,10 +2679,10 @@ Module Barrett256.
           end
     end.
 
-    2 : {
+    Focus 2. {
       (* here's where we need to prove the interps are equal even if I change the dead flags *)
-    
-    
+
+
     cbv [barrett_red256_alloc barrett_red256_fancy].
 
     (*
@@ -3396,4 +3396,4 @@ Check prod_barrett_red256_correct.
 Print Assumptions prod_barrett_red256_correct.
 (* The equivalence with generated code is admitted as barrett_red256_alloc_equivalent. *)
 *)
-*)
\ No newline at end of file
+*)