From 3dcf2f79d422f671aadf441c5318994c9cfea6be Mon Sep 17 00:00:00 2001
From: thery
Date: Mon, 21 Jan 2019 18:40:54 +0100
Subject: ring and field simplify can take no arguments

---
 doc/sphinx/proof-engine/tactics.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 59602581c7..554bfefa0a 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4343,7 +4343,7 @@ Automating
    distributivity, constant propagation) and comparing syntactically the
    results.
 
-.. tacn:: ring_simplify {+ @term}
+.. tacn:: ring_simplify {* @term}
    :name: ring_simplify
 
    This tactic applies the normalization procedure described above to
@@ -4357,7 +4357,7 @@ the tactic and how to declare new ring structures. All declared field structures
 can be printed with the ``Print Rings`` command.
 
 .. tacn:: field
-          field_simplify {+ @term}
+          field_simplify {* @term}
           field_simplify_eq
    :name: field; field_simplify; field_simplify_eq
 
-- 
cgit v1.2.3