diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-07 00:04:33 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-07 00:04:33 -0500 |
| commit | b981e12340271bb066a881577d3c7dfaa8aabe25 (patch) | |
| tree | 473b377f10a3724ee8a1be6ef111e79b8514c356 /src/Specific/Framework | |
| parent | 28fc5bf0ee548881f93318aa8bdd9f57a612ee28 (diff) | |
Fix some names
Diffstat (limited to 'src/Specific/Framework')
| -rw-r--r-- | src/Specific/Framework/ArithmeticSynthesis/Defaults.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/Framework/ArithmeticSynthesis/Defaults.v b/src/Specific/Framework/ArithmeticSynthesis/Defaults.v index 4ee04f6a1..023d0821d 100644 --- a/src/Specific/Framework/ArithmeticSynthesis/Defaults.v +++ b/src/Specific/Framework/ArithmeticSynthesis/Defaults.v @@ -123,7 +123,7 @@ Section gen. Defined. Definition constant_sig' v - : { zero : Z^sz | Positional.Fdecode (m:=m) wt zero = v}. + : { c : Z^sz | Positional.Fdecode (m:=m) wt c = v}. Proof. solve_constant_local_sig. Defined. Definition zero_sig' @@ -131,7 +131,7 @@ Section gen. := Eval hnf in constant_sig' _. Definition one_sig' - : { zero : Z^sz | Positional.Fdecode (m:=m) wt zero = 1%F} + : { one : Z^sz | Positional.Fdecode (m:=m) wt one = 1%F} := Eval hnf in constant_sig' _. Definition add_sig' |