diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-03 16:20:33 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-03 16:20:33 -0400 |
| commit | a60260aed203fd5886037d9c3ac8490b83d6bb21 (patch) | |
| tree | 58f67b785d3e2be8620607a89d4f492c5126c8c0 /src/BoundedArithmetic/ArchitectureToZLikeProofs.v | |
| parent | e52fd783c8c1dbfc99ff7e9014c4dfa8f3a8d9c8 (diff) | |
Work around bug #5112 ([Arguments id /] broken)
Diffstat (limited to 'src/BoundedArithmetic/ArchitectureToZLikeProofs.v')
| -rw-r--r-- | src/BoundedArithmetic/ArchitectureToZLikeProofs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/BoundedArithmetic/ArchitectureToZLikeProofs.v b/src/BoundedArithmetic/ArchitectureToZLikeProofs.v index aca1753b7..00ab82ea2 100644 --- a/src/BoundedArithmetic/ArchitectureToZLikeProofs.v +++ b/src/BoundedArithmetic/ArchitectureToZLikeProofs.v @@ -23,7 +23,7 @@ Section fancy_machine_p256_montgomery_foundation. Local Arguments Z.mul !_ !_. Local Arguments BaseSystem.decode !_ !_ / . - Local Arguments BaseSystem.accumulate / . + Local Arguments BaseSystem.accumulate / _ _. Local Arguments BaseSystem.decode' !_ !_ / . Local Ltac introduce_t_step := |