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.

6 files changed, 0 insertions, 676 deletions

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".