From 73563c2ff4a4214a3b6aa2333c3f413086500a0e Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 2 Apr 2020 15:37:24 +0200
Subject: Remove deprecated -require option.

This option is confusing because it does Require Import, not Require.
It was deprecated in 8.11.  We remove it in 8.12 in order to
reintroduce it in 8.13 as a replacement for -load-vernac-object, which
is the option that does Require without Import as of today.
---
 doc/sphinx/practical-tools/coq-commands.rst | 1 -
 1 file changed, 1 deletion(-)

(limited to 'doc')

diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index aa4b6edd7d..85ed0112ae 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -172,7 +172,6 @@ and ``coqtop``, unless stated otherwise:
   This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`.
 :-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it.
   This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Export` :n:`@qualid`.
-:-require *qualid*: Deprecated; use ``-ri`` *qualid*.
 :-batch: Exit just after argument parsing. Available for ``coqtop`` only.
 :-compile *file.v*: Deprecated; use ``coqc`` instead. Compile file *file.v* into *file.vo*. This option
   implies -batch (exit just after argument parsing). It is available only
-- 
cgit v1.2.3