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.

15 files changed, 14 insertions, 964 deletions

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index d9136ee24b..bac6ccd823 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -168,8 +168,6 @@
 /plugins/syntax/        @ppedrot
 # Secondary maintainer @maximedenes
 
-/plugins/quote/ @herbelin
-
 /plugins/rtauto/       @PierreCorbineau
 # Secondary maintainer @herbelin
 
diff --git a/CHANGES b/CHANGES
index bca4788058..ff242fe285 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,13 @@
+Changes beyond 8.9
+==================
+
+Plugins
+
+- The quote plugin (https://coq.inria.fr/distrib/V8.8.1/refman/proof-engine/detailed-tactic-examples.html#quote)
+  was removed. If some users are interested in maintaining this plugin
+  externally, the Coq development team can provide assistance for extracting
+  the plugin and setting up a new repository.
+
 Changes from 8.8.2 to 8.9+beta1
 ===============================
 
diff --git a/CREDITS b/CREDITS
index 9c3a93da87..3010adc3e1 100644
--- a/CREDITS
+++ b/CREDITS
@@ -50,8 +50,6 @@ plugins/nsatz
   developed by Loïc Pottier (INRIA-Marelle, 2009-2011)
 plugins/omega
   developed by Pierre Crégut (France Telecom R&D, 1996)
-plugins/quote
-  developed by Patrick Loiseleur (LRI, 1997-1999)
 plugins/romega
   developed by Pierre Crégut (France Telecom R&D, 2001-2004)
 plugins/rtauto
diff --git a/META.coq.in b/META.coq.in
index e942267ad7..a7bf08ec49 100644
--- a/META.coq.in
+++ b/META.coq.in
@@ -325,24 +325,12 @@ package "plugins" (
     archive(native)  = "micromega_plugin.cmx"
   )
 
-  package "quote" (
-
-    description = "Coq quote plugin"
-    version     = "8.10"
-
-    requires    = "coq.plugins.ltac"
-    directory   = "quote"
-
-    archive(byte)    = "quote_plugin.cmo"
-    archive(native)  = "quote_plugin.cmx"
-  )
-
   package "newring" (
 
     description = "Coq newring plugin"
     version     = "8.10"
 
-    requires    = "coq.plugins.quote"
+    requires    = ""
     directory   = "setoid_ring"
 
     archive(byte)    = "newring_plugin.cmo"
diff --git a/Makefile.common b/Makefile.common
index 09457ced7b..69dea1d284 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -95,7 +95,7 @@ CORESRCDIRS:=\
   tactics 	vernac		stm		toplevel
 
 PLUGINDIRS:=\
-  omega		romega 		micromega 	quote \
+  omega		romega 		micromega \
   setoid_ring 	extraction \
   cc 		funind 		firstorder 	derive \
   rtauto 	nsatz           syntax          btauto \
@@ -131,7 +131,6 @@ GRAMMARCMA:=grammar/grammar.cma
 OMEGACMO:=plugins/omega/omega_plugin.cmo
 ROMEGACMO:=plugins/romega/romega_plugin.cmo
 MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo
-QUOTECMO:=plugins/quote/quote_plugin.cmo
 RINGCMO:=plugins/setoid_ring/newring_plugin.cmo
 NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo
 EXTRACTIONCMO:=plugins/extraction/extraction_plugin.cmo
@@ -152,7 +151,7 @@ SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
 SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
 
 PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
-        $(QUOTECMO) $(RINGCMO) \
+        $(RINGCMO) \
         $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
         $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \
diff --git a/Makefile.dev b/Makefile.dev
index 7fc1076a8f..2a7e61126a 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -171,7 +171,6 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \
 OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO))
 ROMEGAVO:=$(filter plugins/romega/%, $(PLUGINSVO))
 MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO))
-QUOTEVO:=$(filter plugins/quote/%, $(PLUGINSVO))
 RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO))
 NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO))
 FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO))
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
 -----------------
 
diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v
deleted file mode 100644
index 2d3d9170c1..0000000000
--- a/plugins/quote/Quote.v
+++ /dev/null
@@ -1,86 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-Declare ML Module "quote_plugin".
-
-(***********************************************************************
-  The "abstract" type index is defined to represent variables.
-
-  index : Set
-  index_eq : index -> bool
-  index_eq_prop: (n,m:index)(index_eq n m)=true -> n=m
-  index_lt : index -> bool
-  varmap : Type -> Type.
-  varmap_find : (A:Type)A -> index -> (varmap A) -> A.
-
-  The first arg. of varmap_find is the default value to take
-  if the object is not found in the varmap.
-
-  index_lt defines a total well-founded order, but we don't prove that.
-
-***********************************************************************)
-
-Set Implicit Arguments.
-
-Section variables_map.
-
-Variable A : Type.
-
-Inductive varmap : Type :=
-  | Empty_vm : varmap
-  | Node_vm : A -> varmap -> varmap -> varmap.
-
-Inductive index : Set :=
-  | Left_idx : index -> index
-  | Right_idx : index -> index
-  | End_idx : index.
-
-Fixpoint varmap_find (default_value:A) (i:index) (v:varmap) {struct v} : A :=
-  match i, v with
-  | End_idx, Node_vm x _ _ => x
-  | Right_idx i1, Node_vm x v1 v2 => varmap_find default_value i1 v2
-  | Left_idx i1, Node_vm x v1 v2 => varmap_find default_value i1 v1
-  | _, _ => default_value
-  end.
-
-Fixpoint index_eq (n m:index) {struct m} : bool :=
-  match n, m with
-  | End_idx, End_idx => true
-  | Left_idx n', Left_idx m' => index_eq n' m'
-  | Right_idx n', Right_idx m' => index_eq n' m'
-  | _, _ => false
-  end.
-
-Fixpoint index_lt (n m:index) {struct m} : bool :=
-  match n, m with
-  | End_idx, Left_idx _ => true
-  | End_idx, Right_idx _ => true
-  | Left_idx n', Right_idx m' => true
-  | Right_idx n', Right_idx m' => index_lt n' m'
-  | Left_idx n', Left_idx m' => index_lt n' m'
-  | _, _ => false
-  end.
-
-Lemma index_eq_prop : forall n m:index, index_eq n m = true -> n = m.
-  simple induction n; simple induction m; simpl; intros.
-  rewrite (H i0 H1); reflexivity.
-  discriminate.
-  discriminate.
-  discriminate.
-  rewrite (H i0 H1); reflexivity.
-  discriminate.
-  discriminate.
-  discriminate.
-  reflexivity.
-Qed.
-
-End variables_map.
-
-Unset Implicit Arguments.
diff --git a/plugins/quote/g_quote.mlg b/plugins/quote/g_quote.mlg
deleted file mode 100644
index 749903c3ad..0000000000
--- a/plugins/quote/g_quote.mlg
+++ /dev/null
@@ -1,46 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-{
-
-open Ltac_plugin
-open Names
-open Tacexpr
-open Geninterp
-open Quote
-open Stdarg
-open Tacarg
-
-}
-
-DECLARE PLUGIN "quote_plugin"
-
-{
-
-let cont = Id.of_string "cont"
-let x = Id.of_string "x"
-
-let make_cont (k : Val.t) (c : EConstr.t) =
-  let c = Tacinterp.Value.of_constr c in
-  let tac = TacCall (Loc.tag (Locus.ArgVar CAst.(make cont), [Reference (Locus.ArgVar CAst.(make x))])) in
-  let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in
-  Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac))
-
-}
-
-TACTIC EXTEND quote
-| [ "quote" ident(f) ] -> { quote f [] }
-| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> { quote f lc }
-| [ "quote" ident(f) "in" constr(c) "using" tactic(k) ] ->
-  { gen_quote (make_cont k) c f [] }
-| [ "quote" ident(f) "[" ne_ident_list(lc) "]"
-    "in" constr(c) "using" tactic(k) ] ->
-  { gen_quote (make_cont k) c f lc }
-END
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
deleted file mode 100644
index 7464b42dc5..0000000000
--- a/plugins/quote/quote.ml
+++ /dev/null
@@ -1,540 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* The `Quote' tactic *)
-
-(* The basic idea is to automatize the inversion of interpretation functions
-   in 2-level approach
-
-   Examples are given in \texttt{theories/DEMOS/DemoQuote.v}
-
-   Suppose you have a langage \texttt{L} of 'abstract terms'
-   and a type \texttt{A} of 'concrete terms'
-   and a function \texttt{f : L -> (varmap A L) -> A}.
-
-   Then, the tactic \texttt{quote f} will replace an
-   expression \texttt{e} of type \texttt{A} by \texttt{(f vm t)}
-   such that \texttt{e} and \texttt{(f vm t)} are convertible.
-
-   The problem is then inverting the function \texttt{f}.
-
-   The tactic works when:
-
-   \begin{itemize}
-   \item L is a simple inductive datatype. The constructors of L may
-     have one of the three following forms:
-
-     \begin{enumerate}
-     \item ordinary recursive constructors like: \verb|Cplus : L -> L -> L|
-     \item variable leaf like: \verb|Cvar : index -> L|
-     \item constant leaf like \verb|Cconst : A -> L|
-     \end{enumerate}
-
-     The definition of \texttt{L} must contain at most one variable
-     leaf and at most one constant leaf.
-
-     When there are both a variable leaf and a constant leaf, there is
-     an ambiguity on inversion. The term t can be either the
-     interpretation of \texttt{(Cconst t)} or the interpretation of
-     (\texttt{Cvar}~$i$) in a variable map containing the binding $i
-     \rightarrow$~\texttt{t}. How to discriminate between these
-     choices?
-
-     To solve the dilemma, one gives to \texttt{quote} a list of
-     \emph{constant constructors}: a term will be considered as a
-     constant if it is either a constant constructor or the
-     application of a constant constructor to constants. For example
-     the list \verb+[S, O]+ defines the closed natural
-     numbers. \texttt{(S (S O))} is a constant when \texttt{(S x)} is
-     not.
-
-     The definition of constants vary for each application of the
-     tactic, so it can even be different for two applications of
-     \texttt{quote} with the same function.
-
-   \item \texttt{f} is a quite simple fixpoint on
-     \texttt{L}. In particular, \texttt{f} must verify:
-
-\begin{verbatim}
-     (f (Cvar i)) = (varmap_find vm default_value i)
-\end{verbatim}
-\begin{verbatim}
-     (f (Cconst c)) = c
-\end{verbatim}
-
-     where \texttt{index} and \texttt{varmap\_find} are those defined
-     the \texttt{Quote} module. \emph{The tactic won't work with
-     user's own variables map!!}  It is mandatory to use the
-     variable map defined in module \texttt{Quote}.
-
-   \end{itemize}
-
-   The method to proceed is then clear:
-
-   \begin{itemize}
-   \item Start with an empty hashtable of "registed leafs"
-      that maps constr to integers and a "variable counter" equal to 0.
-    \item Try to match the term with every right hand side of the
-      definition of \texttt{f}.
-
-      If there is one match, returns the correponding left hand
-      side and call yourself recursively to get the arguments of this
-      left hand side.
-
-      If there is no match, we are at a leaf. That is the
-      interpretation of either a variable or a constant.
-
-      If it is a constant, return \texttt{Cconst} applied to that
-      constant.
-
-      If not, it is a variable. Look in the hashtable
-      if this leaf has been already encountered. If not, increment
-      the variable counter and add an entry to the hashtable; then
-      return \texttt{(Cvar !variables\_counter)}
-   \end{itemize}
-*)
-
-
-(*i*)
-open CErrors
-open Util
-open Names
-open Constr
-open EConstr
-open Pattern
-open Patternops
-open Constr_matching
-open Tacmach
-open Proofview.Notations
-(*i*)
-
-(*s First, we need to access some Coq constants
-  We do that lazily, because this code can be linked before
-  the constants are loaded in the environment *)
-
-let constant dir s =
-  EConstr.of_constr @@ UnivGen.constr_of_global @@
-    Coqlib.coq_reference "Quote" ("quote"::dir) s
-
-let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm")
-let coq_Node_vm = lazy (constant ["Quote"] "Node_vm")
-let coq_varmap_find = lazy (constant ["Quote"] "varmap_find")
-let coq_Right_idx = lazy (constant ["Quote"] "Right_idx")
-let coq_Left_idx = lazy (constant ["Quote"] "Left_idx")
-let coq_End_idx = lazy (constant ["Quote"] "End_idx")
-
-(*s Then comes the stuff to decompose the body of interpetation function
-  and pre-compute the inversion data.
-
-For a function like:
-
-\begin{verbatim}
-  Fixpoint interp (vm:varmap Prop) (f:form) :=
-     match f with
-       | f_and f1 f1 f2 => (interp f1) /\ (interp f2)
-       | f_or f1 f1 f2 => (interp f1) \/ (interp f2)
-       | f_var i => varmap_find Prop default_v i vm
-       | f_const c => c
-     end.
-\end{verbatim}
-
-With the constant constructors \texttt{C1}, \dots, \texttt{Cn}, the
-corresponding scheme will be:
-
-\begin{verbatim}
-  {normal_lhs_rhs =
-     [ "(f_and ?1 ?2)", "?1 /\ ?2";
-       "(f_or ?1 ?2)", " ?1 \/ ?2";];
-   return_type = "Prop";
-   constants = Some [C1,...Cn];
-   variable_lhs = Some "(f_var ?1)";
-   constant_lhs = Some "(f_const ?1)"
-  }
-\end{verbatim}
-
-If there is no constructor for variables in the type \texttt{form},
-then [variable_lhs] is [None]. Idem for constants and
-[constant_lhs]. Both cannot be equal to [None].
-
-The metas in the RHS must correspond to those in the LHS (one cannot
-exchange ?1 and ?2 in the example above)
-
-*)
-
-module ConstrSet = Set.Make(Constr)
-
-type inversion_scheme = {
-  normal_lhs_rhs : (constr * constr_pattern) list;
-  variable_lhs : constr option;
-  return_type : constr;
-  constants : ConstrSet.t;
-  constant_lhs : constr option }
-
-(*s [compute_ivs gl f cs] computes the inversion scheme associated to
-  [f:constr] with constants list [cs:constr list] in the context of
-  goal [gl]. This function uses the auxiliary functions
-  [i_can't_do_that], [decomp_term], [compute_lhs] and [compute_rhs]. *)
-
-let i_can't_do_that () = user_err Pp.(str "Quote: not a simple fixpoint")
-
-let decomp_term sigma c = EConstr.kind sigma (Termops.strip_outer_cast sigma c)
-
-(*s [compute_lhs typ i nargsi] builds the term \texttt{(C ?nargsi ...
-  ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive
-  type [typ] *)
-
-let coerce_meta_out id =
-  let s = Id.to_string id in
-  int_of_string (String.sub s 1 (String.length s - 1))
-let coerce_meta_in n =
-  Id.of_string ("M" ^ string_of_int n)
-
-let compute_lhs sigma typ i nargsi =
-  match EConstr.kind sigma typ with
-    | Ind((sp,0),u) ->
-        let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in
-        mkApp (mkConstructU (((sp,0),i+1),u), argsi)
-    | _ -> i_can't_do_that ()
-
-(*s This function builds the pattern from the RHS. Recursive calls are
-  replaced by meta-variables ?i corresponding to those in the LHS *)
-
-let compute_rhs env sigma bodyi index_of_f =
-  let rec aux c =
-    match EConstr.kind sigma c with
-      | App (j, args) when isRel sigma j && Int.equal (destRel sigma j) index_of_f (* recursive call *) ->
-          let i = destRel sigma (Array.last args) in
-	  PMeta (Some (coerce_meta_in i))
-      | App (f,args) ->
-          PApp (pattern_of_constr env sigma (EConstr.to_constr sigma f), Array.map aux args)
-      | Cast (c,_,_) -> aux c
-      | _ -> pattern_of_constr env sigma (EConstr.to_constr sigma c)
-  in
-  aux bodyi
-
-(*s Now the function [compute_ivs] itself *)
-
-let compute_ivs f cs gl =
-  let env = Proofview.Goal.env gl in
-  let sigma = Tacmach.New.project gl in
-  let (cst, u) = try destConst sigma f with DestKO -> i_can't_do_that () in
-  let u = EInstance.kind sigma u in
-  let body = Environ.constant_value_in (Global.env()) (cst, u) in
-  let body = EConstr.of_constr body in
-  match decomp_term sigma body with
-    | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
-        let (args3, body3) = decompose_lam sigma body2 in
-        let nargs3 = List.length args3 in
-        let is_conv = Reductionops.is_conv env sigma in
-          begin match decomp_term sigma body3 with
-          | Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *)
-              let n_lhs_rhs = ref []
-              and v_lhs = ref (None : constr option)
-              and c_lhs = ref (None : constr option) in
-              Array.iteri
-                (fun i ci ->
-                   let argsi, bodyi = decompose_lam sigma ci in
-                   let nargsi = List.length argsi in
-           (* REL (narg3 + nargsi + 1) is f *)
-           (* REL nargsi+1 to REL nargsi + nargs3 are arguments of f *)
-           (* REL 1 to REL nargsi are argsi (reverse order) *)
-           (* First we test if the RHS is the RHS for constants *)
-                   if isRel sigma bodyi && Int.equal (destRel sigma bodyi) 1 then
-                     c_lhs := Some (compute_lhs sigma (snd (List.hd args3))
-                                      i nargsi)
-           (* Then we test if the RHS is the RHS for variables *)
-                   else begin match decompose_app sigma bodyi with
-                     | vmf, [_; _; a3; a4 ]
-                         when isRel sigma a3 && isRel sigma a4 && is_conv vmf
-                           (Lazy.force coq_varmap_find) ->
-                             v_lhs := Some (compute_lhs sigma
-                                              (snd (List.hd args3))
-                                              i nargsi)
-           (* Third case: this is a normal LHS-RHS *)
-                     | _ ->
-                         n_lhs_rhs :=
-                         (compute_lhs sigma (snd (List.hd args3)) i nargsi,
-                          compute_rhs env sigma bodyi (nargs3 + nargsi + 1))
-                         :: !n_lhs_rhs
-                   end)
-                lci;
-
-              if Option.is_empty !c_lhs && Option.is_empty !v_lhs then i_can't_do_that ();
-
-	      (* The Cases predicate is a lambda; we assume no dependency *)
-	      let p = match EConstr.kind sigma p with
-		| Lambda (_,_,p) -> Termops.pop p
-		| _ -> p
-	      in
-
-              { normal_lhs_rhs = List.rev !n_lhs_rhs;
-                variable_lhs = !v_lhs;
-                return_type = p;
-                constants = List.fold_right ConstrSet.add cs ConstrSet.empty;
-                constant_lhs = !c_lhs }
-
-          | _ -> i_can't_do_that ()
-        end
-    |_ -> i_can't_do_that ()
-
-(* TODO for that function:
-\begin{itemize}
-\item handle the case where the return type is an argument of the
-  function
-\item handle the case of simple mutual inductive (for example terms
-  and lists of terms) formulas with the corresponding mutual
-  recursvive interpretation functions.
-\end{itemize}
-*)
-
-(*s Stuff to build variables map, currently implemented as complete
-binary search trees (see file \texttt{Quote.v}) *)
-
-(* First the function to distinghish between constants (closed terms)
-   and variables (open terms) *)
-
-let rec closed_under sigma cset t =
-  (ConstrSet.mem (EConstr.Unsafe.to_constr t) cset) ||
-  (match EConstr.kind sigma t with
-     | Cast(c,_,_) -> closed_under sigma cset c
-     | App(f,l) -> closed_under sigma cset f && Array.for_all (closed_under sigma cset) l
-     | _ -> false)
-
-(*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete
-   binary search tree containing the [ci], that is:
-
-\begin{verbatim}
-                  c1
-                 /  \
-               c2    c3
-              /  \
-             c4  c5
-\end{verbatim}
-
-The second argument is a constr (the common type of the [ci])
-*)
-
-let btree_of_array a ty =
-  let size_of_a = Array.length a in
-  let semi_size_of_a = size_of_a lsr 1 in
-  let node = Lazy.force coq_Node_vm
-  and empty = mkApp (Lazy.force coq_Empty_vm, [| ty |]) in
-  let rec aux n =
-    if n > size_of_a
-    then empty
-    else if  n > semi_size_of_a
-    then mkApp (node, [| ty; a.(n-1); empty; empty |])
-    else mkApp (node, [| ty; a.(n-1); aux (2*n); aux (2*n+1) |])
-  in
-  aux 1
-
-(*s [btree_of_array] and [path_of_int] verify the following invariant:\\
-   {\tt (varmap\_find A dv }[(path_of_int n)] [(btree_of_array a ty)]
-  = [a.(n)]\\
-  [n] must be [> 0] *)
-
-let path_of_int n =
-  (* returns the list of digits of n in reverse order with
-     initial 1 removed *)
-  let rec digits_of_int n =
-    if Int.equal n 1 then []
-    else (Int.equal (n mod 2) 1)::(digits_of_int (n lsr 1))
-  in
-  List.fold_right
-    (fun b c -> mkApp ((if b then Lazy.force coq_Right_idx
-                         else Lazy.force coq_Left_idx),
-                         [| c |]))
-    (List.rev (digits_of_int n))
-    (Lazy.force coq_End_idx)
-
-(*s The tactic works with a list of subterms sharing the same
-  variables map. We need to sort terms in order to avoid than
-  strange things happen during replacement of terms by their
-  'abstract' counterparties. *)
-
-(* [subterm t t'] tests if constr [t'] occurs in [t] *)
-(* This function does not descend under binders (lambda and Cases) *)
-
-let rec subterm gl (t : constr) (t' : constr) =
-  (pf_conv_x gl t t') ||
-  (match EConstr.kind (project gl) t with
-     | App (f,args) -> Array.exists (fun t -> subterm gl t t') args
-     | Cast(t,_,_) -> (subterm gl t t')
-     | _ -> false)
-
-(*s We want to sort the list according to reverse subterm order. *)
-(* Since it's a partial order the algoritm of Sort.list won't work !! *)
-
-let rec sort_subterm gl l =
-  let sigma = project gl in
-  let rec insert c = function
-    | [] -> [c]
-    | (h::t as l) when EConstr.eq_constr sigma c h -> l (* Avoid doing the same work twice *)
-    | h::t -> if subterm gl c h then c::h::t else h::(insert c t)
-  in
-  match l with
-    | [] -> []
-    | h::t -> insert h (sort_subterm gl t)
-
-module Constrhash = Hashtbl.Make(Constr)
-
-let subst_meta subst c =
-  let subst = List.map (fun (i, c) -> i, EConstr.Unsafe.to_constr c) subst in
-  EConstr.of_constr (Termops.subst_meta subst (EConstr.Unsafe.to_constr c))
-
-(*s Now we are able to do the inversion itself.
-  We destructurate the term and use an imperative hashtable
-  to store leafs that are already encountered.
-  The type of arguments is:\\
-  [ivs : inversion_scheme]\\
-  [lc: constr list]\\
-  [gl: goal sigma]\\ *)
-let quote_terms env sigma ivs lc =
-  Coqlib.check_required_library ["Coq";"quote";"Quote"];
-  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
-  let varlist = ref ([] : constr list) in (* list of variables *)
-  let counter = ref 1 in (* number of variables created + 1 *)
-  let rec aux c =
-    let rec auxl l =
-      match l with
-        | (lhs, rhs)::tail ->
-            begin try
-              let s1 = Id.Map.bindings (matches env sigma rhs c) in
-              let s2 = List.map (fun (i,c_i) -> (coerce_meta_out i,aux c_i)) s1
-	      in
-              subst_meta s2 lhs
-            with PatternMatchingFailure -> auxl tail
-            end
-        |  [] ->
-             begin match ivs.variable_lhs with
-               | None ->
-                   begin match ivs.constant_lhs with
-                     | Some c_lhs -> subst_meta [1, c] c_lhs
-                     | None -> anomaly (Pp.str "invalid inversion scheme for quote.")
-                   end
-               | Some var_lhs ->
-                   begin match ivs.constant_lhs with
-                     | Some c_lhs when closed_under sigma ivs.constants c ->
-			 subst_meta [1, c] c_lhs
-                     | _ ->
-			 begin
-                           try Constrhash.find varhash (EConstr.Unsafe.to_constr c)
-                           with Not_found ->
-                             let newvar =
-                               subst_meta [1, (path_of_int !counter)]
-				 var_lhs in
-                             begin
-                               incr counter;
-                               varlist := c :: !varlist;
-                               Constrhash.add varhash (EConstr.Unsafe.to_constr c) newvar;
-                               newvar
-                             end
-			 end
-                   end
-             end
-    in
-    auxl ivs.normal_lhs_rhs
-  in
-  let lp = List.map aux lc in
-    (lp, (btree_of_array (Array.of_list (List.rev !varlist))
-            ivs.return_type ))
-
-(*s actually we could "quote" a list of terms instead of a single
-  term. Ring for example needs that, but Ring doesn't use Quote
-  yet. *)
-
-let pf_constrs_of_globals l =
-  let rec aux l acc =
-    match l with
-      [] -> Proofview.tclUNIT (List.rev acc)
-    | hd :: tl ->
-       Tacticals.New.pf_constr_of_global hd >>= fun g -> aux tl (g :: acc)
-  in aux l []
-
-let quote f lid =
-  Proofview.Goal.enter begin fun gl ->
-    let fg = Tacmach.New.pf_global f gl in
-    let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
-    Tacticals.New.pf_constr_of_global fg >>= fun f ->
-    pf_constrs_of_globals clg >>= fun cl ->
-    Proofview.Goal.nf_enter begin fun gl ->
-      let env = Proofview.Goal.env gl in
-      let sigma = Tacmach.New.project gl in
-      let ivs = compute_ivs f (List.map (EConstr.to_constr sigma) cl) gl in
-      let concl = Proofview.Goal.concl gl in
-      let quoted_terms = quote_terms env sigma ivs [concl] in
-      let (p, vm) = match quoted_terms with
-      | [p], vm -> (p,vm)
-      | _ -> assert false
-      in
-      match ivs.variable_lhs with
-      | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast
-      | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast
-    end
-  end
-
-let gen_quote cont c f lid =
-  Proofview.Goal.enter begin fun gl ->
-    let fg = Tacmach.New.pf_global f gl in
-    let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
-    Tacticals.New.pf_constr_of_global fg >>= fun f ->
-    pf_constrs_of_globals clg >>= fun cl ->
-    Proofview.Goal.nf_enter begin fun gl ->
-      let env = Proofview.Goal.env gl in
-      let sigma = Tacmach.New.project gl in
-      let cl = List.map (EConstr.to_constr sigma) cl in
-      let ivs = compute_ivs f cl gl in
-      let quoted_terms = quote_terms env sigma ivs [c] in
-      let (p, vm) = match quoted_terms with
-        | [p], vm -> (p,vm)
-        | _ -> assert false
-      in
-      match ivs.variable_lhs with
-      | None -> cont (mkApp (f, [| p |]))
-      | Some _ -> cont (mkApp (f, [| vm; p |]))
-    end
-  end
-
-(*i
-
-Just testing ...
-
-#use "include.ml";;
-open Quote;;
-
-let r = glob_constr_of_string;;
-
-let ivs = {
-  normal_lhs_rhs =
-   [ r "(f_and ?1 ?2)", r "?1/\?2";
-     r "(f_not ?1)", r "~?1"];
-  variable_lhs = Some (r "(f_atom ?1)");
-  return_type = r "Prop";
-  constants = ConstrSet.empty;
-  constant_lhs = (r "nat")
-};;
-
-let t1 = r "True/\(True /\ ~False)";;
-let t2 = r "True/\~~False";;
-
-quote_term ivs () t1;;
-quote_term ivs () t2;;
-
-let ivs2 =
-  normal_lhs_rhs =
-   [ r "(f_and ?1 ?2)", r "?1/\?2";
-     r "(f_not ?1)", r "~?1"
-     r "True", r "f_true"];
-  variable_lhs = Some (r "(f_atom ?1)");
-  return_type = r "Prop";
-  constants = ConstrSet.empty;
-  constant_lhs = (r "nat")
-
-i*)
diff --git a/plugins/quote/quote_plugin.mlpack b/plugins/quote/quote_plugin.mlpack
deleted file mode 100644
index 2e9be09d8d..0000000000
--- a/plugins/quote/quote_plugin.mlpack
+++ /dev/null
@@ -1,2 +0,0 @@
-Quote
-G_quote
diff --git a/plugins/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v
index a9b4d9d6f4..920b13ef49 100644
--- a/plugins/setoid_ring/Ring_base.v
+++ b/plugins/setoid_ring/Ring_base.v
@@ -12,7 +12,6 @@
    ring tactic. Abstract rings need more theory, depending on
    ZArith_base. *)
 
-Require Import Quote.
 Declare ML Module "newring_plugin".
 Require Export Ring_theory.
 Require Export Ring_tac.
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index e8efb362e2..26fef99bb2 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -15,7 +15,6 @@ Require Import Ring_polynom.
 Require Import BinList.
 Require Export ListTactics.
 Require Import InitialRing.
-Require Import Quote.
 Declare ML Module "newring_plugin".
 
 
diff --git a/test-suite/output/Quote.v b/test-suite/output/Quote.v
deleted file mode 100644
index 2c373d5052..0000000000
--- a/test-suite/output/Quote.v
+++ /dev/null
@@ -1,36 +0,0 @@
-Require Import Quote.
-
-Parameter A B : Prop.
-
-Inductive formula : Type :=
-  | f_and : formula -> formula -> formula
-  | f_or : formula -> formula -> formula
-  | f_not : formula -> formula
-  | f_true : formula
-  | f_atom : index -> formula
-  | f_const : Prop -> formula.
-
-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
-  | f_const c => c
-  end.
-
-Goal A \/ B -> A /\ (B \/ A) /\ (A \/ ~ B).
-intro H.
-match goal with
-  | H : ?a \/ ?b |- _ => quote interp_f in a using (fun x => idtac x; change (x \/ b) in H)
-end.
-match goal with
-  |- ?g => quote interp_f [ A ] in g using (fun x => idtac x)
-end.
-quote interp_f.
-Show.
-simpl; quote interp_f [ A ].
-Show.
-Admitted.