diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-21 13:17:19 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-21 13:17:19 -0500 |
| commit | b7d2af40ff07a4bc88024fa8448672d786cdcd66 (patch) | |
| tree | 30337011c4fc2b6ae2292abaa6c78cb5457226a1 /src/SpecificGen/GF25519_32Reflective/Reified | |
| parent | b10381a153d2b15d767cc8ae7100cd6e1d9715f3 (diff) | |
Rename Interp lemmas
```bash
$ git grep --name-only 'Interp_InlineCast\|Interp_InlineConst\|Interp_Linearize' | xargs sed s'/Interp_/Interp/g' -i
```
Diffstat (limited to 'src/SpecificGen/GF25519_32Reflective/Reified')
| -rw-r--r-- | src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v | 2 | ||||
| -rw-r--r-- | src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v | 2 |
2 files changed, 2 insertions, 2 deletions
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. |