diff options
| author |  jadephilipoom <jade.philipoom@gmail.com> | 2017-05-14 16:24:40 -0400 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2017-05-14 16:24:40 -0400 |
| commit | a6e0ab7466b2f8a717af2a463edc1d72eab99b5e (patch) | |
| tree | 29ead445d913b407cac5047414e30c198148378f | |
| parent | 8a223dbfe035248f2a3dd562a948cb2960993abd (diff) | |
remove lingering [About]
| -rw-r--r-- | src/Specific/ArithmeticSynthesisTest.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/Specific/ArithmeticSynthesisTest.v b/src/Specific/ArithmeticSynthesisTest.v index 94530a414..bc6652df7 100644 --- a/src/Specific/ArithmeticSynthesisTest.v +++ b/src/Specific/ArithmeticSynthesisTest.v @@ -222,7 +222,6 @@ Section Ops51. pose proof div_mod. pose proof wt_divides_full_pos. pose proof wt_multiples. pose proof div_correct. pose proof modulo_correct. - About freeze. let x := constr:(freeze (n:=sz) (div:=div) (modulo:=modulo) wt (Z.ones bitwidth) m_enc a) in F_mod_eq; transitivity (Positional.eval wt x); repeat autounfold; |