Rename Interp lemmas

```bash
$ git grep --name-only 'Interp_InlineCast\|Interp_InlineConst\|Interp_Linearize' | xargs sed s'/Interp_/Interp/g' -i
```

18 files changed, 22 insertions, 22 deletions

diff --git a/src/Reflection/InlineCastInterp.v b/src/Reflection/InlineCastInterp.v
index 1f02c71ea..5cf2bf7fe 100644
--- a/src/Reflection/InlineCastInterp.v
+++ b/src/Reflection/InlineCastInterp.v
@@ -105,9 +105,9 @@ Section language.
 
   Local Hint Resolve interpf_exprf_of_push_cast.
 
-  Lemma Interp_InlineCast {t} e (Hwf : Wf e)
+  Lemma InterpInlineCast {t} e (Hwf : Wf e)
     : interp_type_gen_rel_pointwise (fun _ => @eq _)
                                     (Interp interp_op (@InlineCast t e))
                                     (Interp interp_op e).
-  Proof. apply Interp_InlineConstGen; auto. Qed.
+  Proof. apply InterpInlineConstGen; auto. Qed.
 End language.
diff --git a/src/Reflection/InlineInterp.v b/src/Reflection/InlineInterp.v
index 9743e0426..707a23fee 100644
--- a/src/Reflection/InlineInterp.v
+++ b/src/Reflection/InlineInterp.v
@@ -133,7 +133,7 @@ Section language.
     eapply interp_inline_const_gen; eauto.
   Qed.
 
-  Lemma Interp_InlineConstGen postprocess {t} (e : Expr t)
+  Lemma InterpInlineConstGen postprocess {t} (e : Expr t)
         (wf : Wf e)
         (Hpostprocess : forall t e, interpf interp_op (exprf_of_inline_directive (postprocess _ t e)) = interpf interp_op e)
     : interp_type_gen_rel_pointwise (fun _ => @eq _)
@@ -144,12 +144,12 @@ Section language.
     eapply (interp_inline_const_gen (postprocess _)); simpl in *; intuition (simpl in *; intuition eauto).
   Qed.
 
-  Lemma Interp_InlineConst is_const {t} (e : Expr t)
+  Lemma InterpInlineConst is_const {t} (e : Expr t)
         (wf : Wf e)
     : interp_type_gen_rel_pointwise (fun _ => @eq _)
                                     (Interp interp_op (InlineConst is_const e))
                                     (Interp interp_op e).
   Proof.
-    eapply Interp_InlineConstGen; eauto.
+    eapply InterpInlineConstGen; eauto.
   Qed.
 End language.
diff --git a/src/Reflection/LinearizeInterp.v b/src/Reflection/LinearizeInterp.v
index 0f6a161e5..0679fe437 100644
--- a/src/Reflection/LinearizeInterp.v
+++ b/src/Reflection/LinearizeInterp.v
@@ -77,7 +77,7 @@ Section language.
     eapply interpf_linearizef.
   Qed.
 
-  Lemma Interp_Linearize {t} (e : Expr t)
+  Lemma InterpLinearize {t} (e : Expr t)
     : interp_type_gen_rel_pointwise (fun _ => @eq _)
                                     (Interp interp_op (Linearize e))
                                     (Interp interp_op e).
diff --git a/src/Reflection/Z/Reify.v b/src/Reflection/Z/Reify.v
index 63b5832f2..e200b2e9e 100644
--- a/src/Reflection/Z/Reify.v
+++ b/src/Reflection/Z/Reify.v
@@ -43,10 +43,10 @@ Ltac prove_InlineConst_Linearize_Compile_correct :=
      lazymatch goal with
      | [ |- ?R (@Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t (InlineConst ?is_const (Linearize _))) _ ]
        => etransitivity;
-          [ apply (@Interp_InlineConst base_type_code interp_base_type op interp_op is_const t);
+          [ apply (@InterpInlineConst base_type_code interp_base_type op interp_op is_const t);
             reflect_Wf base_type_eq_semidec_is_dec op_beq_bl
           | etransitivity;
-            [ apply (@Interp_Linearize base_type_code interp_base_type op interp_op t)
+            [ apply (@InterpLinearize base_type_code interp_base_type op interp_op t)
             | prove_compile_correct () ] ]
      end.
 Ltac Reify_rhs :=
diff --git a/src/Specific/GF25519Reflective/Reified/AddCoordinates.v b/src/Specific/GF25519Reflective/Reified/AddCoordinates.v
index d35a0e5e9..e14c6c239 100644
--- a/src/Specific/GF25519Reflective/Reified/AddCoordinates.v
+++ b/src/Specific/GF25519Reflective/Reified/AddCoordinates.v
@@ -119,7 +119,7 @@ Qed.
 Lemma radd_coordinatesZ_sigP : rexpr_sigP Expr9_4OpT uncurried_add_coordinates radd_coordinatesZ''.
 Proof.
   cbv [radd_coordinatesZ''].
-  etransitivity; [ apply Interp_Linearize | ].
+  etransitivity; [ apply InterpLinearize | ].
   cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe25519 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519 add_coordinates].
   intros.
   unfold invert_Return at 13 14 15 16.
diff --git a/src/Specific/GF25519Reflective/Reified/LadderStep.v b/src/Specific/GF25519Reflective/Reified/LadderStep.v
index d82ac17ae..bab53cc52 100644
--- a/src/Specific/GF25519Reflective/Reified/LadderStep.v
+++ b/src/Specific/GF25519Reflective/Reified/LadderStep.v
@@ -124,7 +124,7 @@ Qed.
 Lemma rladderstepZ_sigP : rexpr_sigP Expr9_4OpT uncurried_ladderstep rladderstepZ''.
 Proof.
   cbv [rladderstepZ''].
-  etransitivity; [ apply Interp_Linearize | ].
+  etransitivity; [ apply InterpLinearize | ].
   cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe25519 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519 ladderstep].
   intros; cbv beta zeta.
   unfold invert_Return at 14 15 16 17.
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v
index a51afcf06..84ac36861 100644
--- a/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v
@@ -119,7 +119,7 @@ Qed.
 Lemma radd_coordinatesZ_sigP : rexpr_sigP Expr9_4OpT uncurried_add_coordinates radd_coordinatesZ''.
 Proof.
   cbv [radd_coordinatesZ''].
-  etransitivity; [ apply Interp_Linearize | ].
+  etransitivity; [ apply InterpLinearize | ].
   cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe2213_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe2213_32 add_coordinates].
   intros.
   unfold invert_Return at 13 14 15 16.
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v
index 1ac755508..f4fa2daff 100644
--- a/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v
@@ -124,7 +124,7 @@ Qed.
 Lemma rladderstepZ_sigP : rexpr_sigP Expr9_4OpT uncurried_ladderstep rladderstepZ''.
 Proof.
   cbv [rladderstepZ''].
-  etransitivity; [ apply Interp_Linearize | ].
+  etransitivity; [ apply InterpLinearize | ].
   cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe2213_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe2213_32 ladderstep].
   intros; cbv beta zeta.
   unfold invert_Return at 14 15 16 17.
diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF2519_32Reflective/Reified/AddCoordinates.v
index 5033de383..6c0ee65e7 100644
--- a/src/SpecificGen/GF2519_32Reflective/Reified/AddCoordinates.v
+++ b/src/SpecificGen/GF2519_32Reflective/Reified/AddCoordinates.v
@@ -119,7 +119,7 @@ Qed.
 Lemma radd_coordinatesZ_sigP : rexpr_sigP Expr9_4OpT uncurried_add_coordinates radd_coordinatesZ''.
 Proof.
   cbv [radd_coordinatesZ''].
-  etransitivity; [ apply Interp_Linearize | ].
+  etransitivity; [ apply InterpLinearize | ].
   cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe2519_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe2519_32 add_coordinates].
   intros.
   unfold invert_Return at 13 14 15 16.
diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v
index c06a2cb59..b29f1822b 100644
--- a/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v
+++ b/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v
@@ -124,7 +124,7 @@ Qed.
 Lemma rladderstepZ_sigP : rexpr_sigP Expr9_4OpT uncurried_ladderstep rladderstepZ''.
 Proof.
   cbv [rladderstepZ''].
-  etransitivity; [ apply Interp_Linearize | ].
+  etransitivity; [ apply InterpLinearize | ].
   cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe2519_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe2519_32 ladderstep].
   intros; cbv beta zeta.
   unfold invert_Return at 14 15 16 17.
diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v
index d5c05a6e5..e013a84e5 100644
--- a/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v
+++ b/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v
@@ -119,7 +119,7 @@ Qed.
 Lemma radd_coordinatesZ_sigP : rexpr_sigP Expr9_4OpT uncurried_add_coordinates radd_coordinatesZ''.
 Proof.
   cbv [radd_coordinatesZ''].
-  etransitivity; [ apply Interp_Linearize | ].
+  etransitivity; [ apply InterpLinearize | ].
   cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe25519_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519_32 add_coordinates].
   intros.
   unfold invert_Return at 13 14 15 16.
diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v
index 9f133bb39..ae71337fd 100644
--- a/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v
+++ b/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v
@@ -124,7 +124,7 @@ Qed.
 Lemma rladderstepZ_sigP : rexpr_sigP Expr9_4OpT uncurried_ladderstep rladderstepZ''.
 Proof.
   cbv [rladderstepZ''].
-  etransitivity; [ apply Interp_Linearize | ].
+  etransitivity; [ apply InterpLinearize | ].
   cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe25519_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519_32 ladderstep].
   intros; cbv beta zeta.
   unfold invert_Return at 14 15 16 17.
diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v
index 3303a53bb..0f41ed239 100644
--- a/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v
+++ b/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v
@@ -119,7 +119,7 @@ Qed.
 Lemma radd_coordinatesZ_sigP : rexpr_sigP Expr9_4OpT uncurried_add_coordinates radd_coordinatesZ''.
 Proof.
   cbv [radd_coordinatesZ''].
-  etransitivity; [ apply Interp_Linearize | ].
+  etransitivity; [ apply InterpLinearize | ].
   cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe25519_64 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519_64 add_coordinates].
   intros.
   unfold invert_Return at 13 14 15 16.
diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v
index 33dab7528..66d998d08 100644
--- a/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v
+++ b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v
@@ -124,7 +124,7 @@ Qed.
 Lemma rladderstepZ_sigP : rexpr_sigP Expr9_4OpT uncurried_ladderstep rladderstepZ''.
 Proof.
   cbv [rladderstepZ''].
-  etransitivity; [ apply Interp_Linearize | ].
+  etransitivity; [ apply InterpLinearize | ].
   cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe25519_64 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519_64 ladderstep].
   intros; cbv beta zeta.
   unfold invert_Return at 14 15 16 17.
diff --git a/src/SpecificGen/GF41417_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF41417_32Reflective/Reified/AddCoordinates.v
index fe50d7a26..0a8480432 100644
--- a/src/SpecificGen/GF41417_32Reflective/Reified/AddCoordinates.v
+++ b/src/SpecificGen/GF41417_32Reflective/Reified/AddCoordinates.v
@@ -119,7 +119,7 @@ Qed.
 Lemma radd_coordinatesZ_sigP : rexpr_sigP Expr9_4OpT uncurried_add_coordinates radd_coordinatesZ''.
 Proof.
   cbv [radd_coordinatesZ''].
-  etransitivity; [ apply Interp_Linearize | ].
+  etransitivity; [ apply InterpLinearize | ].
   cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe41417_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe41417_32 add_coordinates].
   intros.
   unfold invert_Return at 13 14 15 16.
diff --git a/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v
index db671ccb4..0d1cd59cb 100644
--- a/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v
+++ b/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v
@@ -124,7 +124,7 @@ Qed.
 Lemma rladderstepZ_sigP : rexpr_sigP Expr9_4OpT uncurried_ladderstep rladderstepZ''.
 Proof.
   cbv [rladderstepZ''].
-  etransitivity; [ apply Interp_Linearize | ].
+  etransitivity; [ apply InterpLinearize | ].
   cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe41417_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe41417_32 ladderstep].
   intros; cbv beta zeta.
   unfold invert_Return at 14 15 16 17.
diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF5211_32Reflective/Reified/AddCoordinates.v
index 88b4ab0fd..90f391ba5 100644
--- a/src/SpecificGen/GF5211_32Reflective/Reified/AddCoordinates.v
+++ b/src/SpecificGen/GF5211_32Reflective/Reified/AddCoordinates.v
@@ -119,7 +119,7 @@ Qed.
 Lemma radd_coordinatesZ_sigP : rexpr_sigP Expr9_4OpT uncurried_add_coordinates radd_coordinatesZ''.
 Proof.
   cbv [radd_coordinatesZ''].
-  etransitivity; [ apply Interp_Linearize | ].
+  etransitivity; [ apply InterpLinearize | ].
   cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe5211_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe5211_32 add_coordinates].
   intros.
   unfold invert_Return at 13 14 15 16.
diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v
index b047b6cd3..16c0173a0 100644
--- a/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v
+++ b/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v
@@ -124,7 +124,7 @@ Qed.
 Lemma rladderstepZ_sigP : rexpr_sigP Expr9_4OpT uncurried_ladderstep rladderstepZ''.
 Proof.
   cbv [rladderstepZ''].
-  etransitivity; [ apply Interp_Linearize | ].
+  etransitivity; [ apply InterpLinearize | ].
   cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe5211_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe5211_32 ladderstep].
   intros; cbv beta zeta.
   unfold invert_Return at 14 15 16 17.