diff options
Diffstat (limited to 'src/Specific/Framework/MontgomeryReificationTypesPackage.v')
| -rw-r--r-- | src/Specific/Framework/MontgomeryReificationTypesPackage.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/Framework/MontgomeryReificationTypesPackage.v b/src/Specific/Framework/MontgomeryReificationTypesPackage.v index 5b440f0e8..6f9364d6e 100644 --- a/src/Specific/Framework/MontgomeryReificationTypesPackage.v +++ b/src/Specific/Framework/MontgomeryReificationTypesPackage.v @@ -75,7 +75,7 @@ Ltac add_MontgomeryReificationTypes_package pkg := let pkg := add_feBW_of_feBW_small pkg in let pkg := add_phiM pkg in let pkg := add_phiM_small pkg in - Tag.strip_local pkg. + Tag.strip_subst_local pkg. Module MakeMontgomeryReificationTypesPackage (PKG : PrePackage). |