Remove quote plugin

As far as I know, this plugin is untested and barely maintained. I don't
think it has real use cases any more, so let's move it out from the repo
and see if somebody wants to take over and maintain it.

We also remove the documentation, which was telling our users to look at
ring to see an example of reification done using quote, when in fact it
wasn't using it anymore.

2 files changed, 1 insertions, 231 deletions

diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index 72dd79d930..bd16b70d02 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -417,218 +417,8 @@ the optional tactic of the ``Hint Rewrite`` command.
 
       Qed.
 
-.. _quote:
-
-quote
------
-
-The tactic ``quote`` allows using Barendregt’s so-called 2-level approach
-without writing any ML code. Suppose you have a language ``L`` of
-'abstract terms' and a type ``A`` of 'concrete terms' and a function ``f : L -> A``.
-If ``L`` is a simple inductive datatype and ``f`` a simple fixpoint,
-``quote f`` will replace the head of current goal by a convertible term of
-the form ``(f t)``. ``L`` must have a constructor of type: ``A -> L``.
-
-Here is an example:
-
-.. coqtop:: in reset
-
-   Require Import Quote.
-
-.. coqtop:: all
-
-   Parameters A B C : Prop.
-
-.. coqtop:: all
-
-   Inductive formula : Type :=
-            | f_and : formula -> formula -> formula (* binary constructor *)
-            | f_or : formula -> formula -> formula
-            | f_not : formula -> formula (* unary constructor *)
-            | f_true : formula (* 0-ary constructor *)
-            | f_const : Prop -> formula (* constructor for constants *).
-
-.. coqtop:: all
-
-   Fixpoint interp_f (f:formula) : Prop :=
-            match f with
-            | f_and f1 f2 => interp_f f1 /\ interp_f f2
-            | f_or f1 f2 => interp_f f1 \/ interp_f f2
-            | f_not f1 => ~ interp_f f1
-            | f_true => True
-            | f_const c => c
-            end.
-
-.. coqtop:: all
-
-   Goal A /\ (A \/ True) /\ ~ B /\ (A <-> A).
-
-.. coqtop:: all
-
-   quote interp_f.
-
-The algorithm to perform this inversion is: try to match the term with
-right-hand sides expression of ``f``. If there is a match, apply the
-corresponding left-hand side and call yourself recursively on sub-
-terms. If there is no match, we are at a leaf: return the
-corresponding constructor (here ``f_const``) applied to the term.
-
-When ``quote`` is not able to perform inversion properly, it will error out with
-:exn:`quote: not a simple fixpoint`.
-
-
-Introducing variables map
-~~~~~~~~~~~~~~~~~~~~~~~~~
-
-The normal use of quote is to make proofs by reflection: one defines a
-function ``simplify : formula -> formula`` and proves a theorem
-``simplify_ok: (f:formula)(interp_f (simplify f)) -> (interp_f f)``. Then,
-one can simplify formulas by doing:
-
-.. coqtop:: in
-
-       quote interp_f.
-       apply simplify_ok.
-       compute.
-
-But there is a problem with leafs: in the example above one cannot
-write a function that implements, for example, the logical
-simplifications :math:`A \wedge A \rightarrow A` or :math:`A \wedge
-\lnot A \rightarrow \mathrm{False}`. This is because ``Prop`` is
-impredicative.
-
-It is better to use that type of formulas:
-
-.. coqtop:: in reset
-
-   Require Import Quote.
-
-.. coqtop:: in
-
-   Parameters A B C : Prop.
-
-.. coqtop:: all
-
-   Inductive formula : Set :=
-            | f_and : formula -> formula -> formula
-            | f_or : formula -> formula -> formula
-            | f_not : formula -> formula
-            | f_true : formula
-            | f_atom : index -> formula.
-
-``index`` is defined in module ``Quote``. Equality on that type is
-decidable so we are able to simplify :math:`A \wedge A` into :math:`A`
-at the abstract level.
-
-When there are variables, there are bindings, and ``quote`` also
-provides a type ``(varmap A)`` of bindings from index to any set
-``A``, and a function ``varmap_find`` to search in such maps. The
-interpretation function also has another argument, a variables map:
-
-.. coqtop:: all
-
-   Fixpoint interp_f (vm:varmap Prop) (f:formula) {struct f} : Prop :=
-            match f with
-            | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2
-            | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2
-            | f_not f1 => ~ interp_f vm f1
-            | f_true => True
-            | f_atom i => varmap_find True i vm
-            end.
-
-``quote`` handles this second case properly:
-
-.. coqtop:: all
-
-   Goal A /\ (B \/ A) /\ (A \/ ~ B).
-
-.. coqtop:: all
-
-   quote interp_f.
-
-It builds ``vm`` and ``t`` such that ``(f vm t)`` is convertible with the
-conclusion of current goal.
-
-
-Combining variables and constants
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-One can have both variables and constants in abstracts terms; for
-example, this is the case for the :tacn:`ring` tactic. Then one must provide to
-``quote`` a list of *constructors of constants*. For example, if the list
-is ``[O S]`` then closed natural numbers will be considered as constants
-and other terms as variables.
-
-.. coqtop:: in reset
-
-   Require Import Quote.
-
-.. coqtop:: in
-
-   Parameters A B C : Prop.
-
-.. coqtop:: in
-
-   Inductive formula : Type :=
-            | f_and : formula -> formula -> formula
-            | f_or : formula -> formula -> formula
-            | f_not : formula -> formula
-            | f_true : formula
-            | f_const : Prop -> formula (* constructor for constants *)
-            | f_atom : index -> formula.
-
-.. coqtop:: in
-
-   Fixpoint interp_f (vm:varmap Prop) (f:formula) {struct f} : Prop :=
-            match f with
-            | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2
-            | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2
-            | f_not f1 => ~ interp_f vm f1
-            | f_true => True
-            | f_const c => c
-            | f_atom i => varmap_find True i vm
-            end.
-
-.. coqtop:: in
-
-   Goal A /\ (A \/ True) /\ ~ B /\ (C <-> C).
-
-.. coqtop:: all
-
-   quote interp_f [ A B ].
-
-
-.. coqtop:: all
-
-   Undo.
-
-.. coqtop:: all
-
-   quote interp_f [ B C iff ].
-
-.. warning::
-   Since functional inversion is undecidable in the general case,
-   don’t expect miracles from it!
-
-.. tacv:: quote @ident in @term using @tactic
-
-   ``tactic`` must be a functional tactic (starting with ``fun x =>``) and
-   will be called with the quoted version of term according to ``ident``.
-
-.. tacv:: quote @ident [{+ @ident}] in @term using @tactic          
-
-   Same as above, but will use the additional ``ident`` list to chose
-   which subterms are constants (see above).
-
-.. seealso::
-   Comments from the source file ``plugins/quote/quote.ml``
-
-.. seealso::
-   The :tacn:`ring` tactic.
-
-
 Using the tactic language
----------------------------
+-------------------------
 
 
 About the cardinality of the set of natural numbers
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 62a482096c..fb121c82ec 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4217,26 +4217,6 @@ available after a ``Require Import FunInd``.
   functional inversion, this variant allows choosing which :n:`@qualid` is
   inverted.
 
-.. tacn:: quote @ident
-   :name: quote
-
-This kind of inversion has nothing to do with the tactic :tacn:`inversion`
-above. This tactic does :g:`change (@ident t)`, where `t` is a term built in
-order to ensure the convertibility. In other words, it does inversion of the
-function :n:`@ident`. This function must be a fixpoint on a simple recursive
-datatype: see :ref:`quote` for the full details.
-
-
-.. exn:: quote: not a simple fixpoint.
-
-  Happens when quote is not able to perform inversion properly.
-
-
-.. tacv::  quote @ident {* @ident}
-
-  All terms that are built only with :n:`{* @ident}` will be considered by quote
-  as constants rather than variables.
-
 Classical tactics
 -----------------