diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-02 12:55:17 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-02 12:55:17 -0700 |
| commit | 5ffeb9cfac7d6e070c8fc36e22680af4ffcf93ee (patch) | |
| tree | 46e08c357c7ab913ee4974dc3282022aead7249b /src/Util/Tactics.v | |
| parent | c5f6e5947cd9a5a8daec65aeb065200f40f3f7a9 (diff) | |
Fix [ring] reference broken by moving [Require] outside a module
Diffstat (limited to 'src/Util/Tactics.v')
0 files changed, 0 insertions, 0 deletions