Chapter 20: The
Ring
tactic
Patrick Loiseleur and Samuel Boutin
This chapter presents the
Ring
tactic.
20.1 What does this tactic?
20.2 The variables map
20.3 Is it automatic?
20.4 Concrete usage in
Coq
20.5 Add a ring structure
20.6 How does it work?
20.7 History of
Ring
20.8 Discussion
