diff options
| author | Pierre Letouzey | 2018-03-12 17:21:04 +0100 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:53 -0400 |
| commit | 44638cda2f8f7461506a6e5a9a2edf860971f96c (patch) | |
| tree | e8cb2c98cd71838a9b51f91848e035cf4f4f9528 /plugins/syntax | |
| parent | 377188d7bfd27518e6ab47d5017907b1f527a7dd (diff) | |
Decimal: scope name changed dec_(u)int_scope
This avoid a clash with int_scope in ssreflect's ssrint.v
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions