From 4563779bf990cf22d88474a68acf4eb9cfd8d173 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 4 Feb 2020 17:07:34 +0100
Subject: Remove Goptions.opt_name field

The standard use is to repeat the option keywords in lowercase, which
is basically useless.

En passant add doc entry for Dump Arith.
---
 doc/sphinx/addendum/micromega.rst | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'doc')

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index b0197c500c..f706633da9 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -35,6 +35,11 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`,
    use the Simplex method for solving linear goals. If it is not set,
    the decision procedures are using Fourier elimination.
 
+.. opt:: Dump Arith
+
+   This option (unset by default) may be set to a file path where
+   debug info will be written.
+
 .. cmd:: Show Lia Profile
 
    This command prints some statistics about the amount of pivoting
-- 
cgit v1.2.3