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/Algebra.v | |
| parent | c5f6e5947cd9a5a8daec65aeb065200f40f3f7a9 (diff) | |
Fix [ring] reference broken by moving [Require] outside a module
Diffstat (limited to 'src/Algebra.v')
| -rw-r--r-- | src/Algebra.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index 632eeac31..301ac8edb 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1319,7 +1319,7 @@ Ltac only_two_square_roots := end. (*** Tactics for ring equations *) -Require Import Coq.setoid_ring.Ring_tac. +Require Export Coq.setoid_ring.Ring_tac. Ltac ring_simplify_subterms := tac_on_subterms ltac:(fun t => ring_simplify t). Ltac ring_simplify_subterms_in_all := |