Split out Reflection.Equality, change Tflat implicit argument

6 files changed, 12 insertions, 12 deletions

diff --git a/src/SpecificGen/GF2213_32Reflective/Common.v b/src/SpecificGen/GF2213_32Reflective/Common.v
index e5fab2a8d..56e4bc47c 100644
--- a/src/SpecificGen/GF2213_32Reflective/Common.v
+++ b/src/SpecificGen/GF2213_32Reflective/Common.v
@@ -327,8 +327,8 @@ Ltac assoc_right_tuple x so_far :=
 Local Ltac make_args x :=
   let x' := fresh "x'" in
   compute in x |- *;
-  let t := match type of x with @expr _ _ _ _ (Tflat _ ?t) => t end in
-  let t' := match goal with |- @expr _ _ _ _ (Tflat _ ?t) => t end in
+  let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in
+  let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in
   refine (LetIn (UnReturn x) _);
   let x'' := fresh "x''" in
   intro x'';
diff --git a/src/SpecificGen/GF2519_32Reflective/Common.v b/src/SpecificGen/GF2519_32Reflective/Common.v
index 729c79995..dd7be148a 100644
--- a/src/SpecificGen/GF2519_32Reflective/Common.v
+++ b/src/SpecificGen/GF2519_32Reflective/Common.v
@@ -327,8 +327,8 @@ Ltac assoc_right_tuple x so_far :=
 Local Ltac make_args x :=
   let x' := fresh "x'" in
   compute in x |- *;
-  let t := match type of x with @expr _ _ _ _ (Tflat _ ?t) => t end in
-  let t' := match goal with |- @expr _ _ _ _ (Tflat _ ?t) => t end in
+  let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in
+  let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in
   refine (LetIn (UnReturn x) _);
   let x'' := fresh "x''" in
   intro x'';
diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v
index aad67f032..644ed7c92 100644
--- a/src/SpecificGen/GF25519_32Reflective/Common.v
+++ b/src/SpecificGen/GF25519_32Reflective/Common.v
@@ -327,8 +327,8 @@ Ltac assoc_right_tuple x so_far :=
 Local Ltac make_args x :=
   let x' := fresh "x'" in
   compute in x |- *;
-  let t := match type of x with @expr _ _ _ _ (Tflat _ ?t) => t end in
-  let t' := match goal with |- @expr _ _ _ _ (Tflat _ ?t) => t end in
+  let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in
+  let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in
   refine (LetIn (UnReturn x) _);
   let x'' := fresh "x''" in
   intro x'';
diff --git a/src/SpecificGen/GF25519_64Reflective/Common.v b/src/SpecificGen/GF25519_64Reflective/Common.v
index f639aa0b6..c7b1a69fb 100644
--- a/src/SpecificGen/GF25519_64Reflective/Common.v
+++ b/src/SpecificGen/GF25519_64Reflective/Common.v
@@ -327,8 +327,8 @@ Ltac assoc_right_tuple x so_far :=
 Local Ltac make_args x :=
   let x' := fresh "x'" in
   compute in x |- *;
-  let t := match type of x with @expr _ _ _ _ (Tflat _ ?t) => t end in
-  let t' := match goal with |- @expr _ _ _ _ (Tflat _ ?t) => t end in
+  let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in
+  let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in
   refine (LetIn (UnReturn x) _);
   let x'' := fresh "x''" in
   intro x'';
diff --git a/src/SpecificGen/GF41417_32Reflective/Common.v b/src/SpecificGen/GF41417_32Reflective/Common.v
index 62d55b463..b9f98cfba 100644
--- a/src/SpecificGen/GF41417_32Reflective/Common.v
+++ b/src/SpecificGen/GF41417_32Reflective/Common.v
@@ -327,8 +327,8 @@ Ltac assoc_right_tuple x so_far :=
 Local Ltac make_args x :=
   let x' := fresh "x'" in
   compute in x |- *;
-  let t := match type of x with @expr _ _ _ _ (Tflat _ ?t) => t end in
-  let t' := match goal with |- @expr _ _ _ _ (Tflat _ ?t) => t end in
+  let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in
+  let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in
   refine (LetIn (UnReturn x) _);
   let x'' := fresh "x''" in
   intro x'';
diff --git a/src/SpecificGen/GF5211_32Reflective/Common.v b/src/SpecificGen/GF5211_32Reflective/Common.v
index 977710173..396d2cd35 100644
--- a/src/SpecificGen/GF5211_32Reflective/Common.v
+++ b/src/SpecificGen/GF5211_32Reflective/Common.v
@@ -327,8 +327,8 @@ Ltac assoc_right_tuple x so_far :=
 Local Ltac make_args x :=
   let x' := fresh "x'" in
   compute in x |- *;
-  let t := match type of x with @expr _ _ _ _ (Tflat _ ?t) => t end in
-  let t' := match goal with |- @expr _ _ _ _ (Tflat _ ?t) => t end in
+  let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in
+  let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in
   refine (LetIn (UnReturn x) _);
   let x'' := fresh "x''" in
   intro x'';