Reorder Reflection.Z.Syntax

This puts all the definitions first, and then puts the interpretations after that

1 files changed, 9 insertions, 7 deletions

diff --git a/src/Reflection/Z/Syntax.v b/src/Reflection/Z/Syntax.v
index afdd87ba9..288876dc9 100644
--- a/src/Reflection/Z/Syntax.v
+++ b/src/Reflection/Z/Syntax.v
@@ -7,15 +7,8 @@ Export Syntax.Notations.
 Local Set Boolean Equality Schemes.
 Local Set Decidable Equality Schemes.
 Inductive base_type := TZ.
-Definition interp_base_type (v : base_type) : Type :=
-  match v with
-  | TZ => Z
-  end.
 
 Local Notation tZ := (Tbase TZ).
-Local Notation eta x := (fst x, snd x).
-Local Notation eta3 x := (eta (fst x), snd x).
-Local Notation eta4 x := (eta3 (fst x), snd x).
 
 Inductive op : flat_type base_type -> flat_type base_type -> Type :=
 | OpConst (z : Z) : op Unit tZ
@@ -30,6 +23,15 @@ Inductive op : flat_type base_type -> flat_type base_type -> Type :=
 | Cmovne : op (tZ * tZ * tZ * tZ) tZ
 | Cmovle : op (tZ * tZ * tZ * tZ) tZ.
 
+Definition interp_base_type (v : base_type) : Type :=
+  match v with
+  | TZ => Z
+  end.
+
+Local Notation eta x := (fst x, snd x).
+Local Notation eta3 x := (eta (fst x), snd x).
+Local Notation eta4 x := (eta3 (fst x), snd x).
+
 Definition interp_op src dst (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst
   := match f in op src dst return interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst with
      | OpConst v => fun _ => v