diff options
Diffstat (limited to 'src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v')
| -rw-r--r-- | src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v b/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v index 4980f09b9..5ade26d76 100644 --- a/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v +++ b/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v @@ -407,7 +407,7 @@ Ltac add_Montgomery_package pkg := let pkg := add_carry_sig pkg in let pkg := add_freeze_sig pkg in let pkg := add_Mxzladderstep_sig pkg in - Tag.strip_local pkg. + Tag.strip_subst_local pkg. Module MakeMontgomeryPackage (PKG : PrePackage). |