move hints and context outside section (this is what happens when you 'organize' code last-minute and don't check that it still works)

1 files changed, 11 insertions, 12 deletions

diff --git a/src/Specific/ArithmeticSynthesisTest.v b/src/Specific/ArithmeticSynthesisTest.v
index 5decf17da..016bd8fef 100644
--- a/src/Specific/ArithmeticSynthesisTest.v
+++ b/src/Specific/ArithmeticSynthesisTest.v
@@ -222,20 +222,19 @@ Section Ops51.
         apply Z.div_positive_gt_0; auto using wt_pos.
         apply wt_multiples.
     Qed.
+  End PreFreeze.
 
-    Context {select_cps : forall n, Z -> Z^n -> forall {T}, (Z^n->T) -> T}
-            {select : forall n, Z -> Z^n -> Z^n}
-            {select_id : forall n cond x T f, @select_cps n cond x T f = f (select n cond x)}
-            {eval_select : forall n cond x,
-                B.Positional.eval wt (select n cond x) = if dec (cond = 0) then 0 else B.Positional.eval wt x}
-    .
-
-    Hint Rewrite select_id : uncps.
-    Hint Rewrite eval_select : push_basesystem_eval.
+  Context {select_cps : forall n, Z -> Z^n -> forall {T}, (Z^n->T) -> T}
+          {select : forall n, Z -> Z^n -> Z^n}
+          {select_id : forall n cond x T f, @select_cps n cond x T f = f (select n cond x)}
+          {eval_select : forall n cond x,
+              B.Positional.eval wt (select n cond x) = if dec (cond = 0) then 0 else B.Positional.eval wt x}
+  .
 
-    Hint Opaque freeze : uncps.
-    Hint Rewrite freeze_id : uncps.
-  End PreFreeze.
+  Hint Rewrite select_id : uncps.
+  Hint Rewrite eval_select : push_basesystem_eval.
+  Hint Opaque freeze : uncps.
+  Hint Rewrite freeze_id : uncps.
   
   Definition freeze_sig :
     {freeze : (Z^sz -> Z^sz)%type |