Take advantage of natdynlink when available: almost all contribs become loadable plugins

- Any contrib foo leads to contrib/foo/foo_plugin.cmxs (and .cma for bytecode).
- Features that were available without any Require are now loaded systematically
  when launching coqtop (see Coqtop.load_initial_plugins):
     extraction, jprover, cc, ground, dp, recdef, xml
- The other plugins are loaded when a corresponding Require is done:
     quote, ring, field, setoid_ring, omega, romega, micromega, fourier
- I experienced a crash (segfault) while turning subtac into a plugin, so this
  one stays statically linked into coqtop for now
- When the ocaml version doesn't support natdynlink, or if "-natdynlink no"
  is explicitely given to configure, coqtop is statically linked with all of
  the above code as usual. Some messages [Ignore ML file Foo_plugin] may appear.
- How should coqdep handle a "Declare ML Module "foo"" if foo is an archive
  and not a ml file ? For now, we suppose that the foo.{cmxs,cma} are at the
  same location as the .v during the build, but can be moved later in any place of
  the ml loadpath.

This is clearly an experimentation. Feedback most welcome...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11687 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 4 insertions, 596 deletions

diff --git a/contrib/ring/LegacyRing.v b/contrib/ring/LegacyRing.v
index ed1da9c56e..4ae85baf37 100644
--- a/contrib/ring/LegacyRing.v
+++ b/contrib/ring/LegacyRing.v
@@ -13,6 +13,7 @@ Require Export LegacyRing_theory.
 Require Export Quote.
 Require Export Ring_normalize.
 Require Export Ring_abstract.
+Declare ML Module "ring_plugin".
 
 (* As an example, we provide an instantation for bool. *)
 (* Other instatiations are given in ArithRing and ZArithRing in the
diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v
deleted file mode 100644
index 9a11a70b9c..0000000000
--- a/contrib/ring/Quote.v
+++ /dev/null
@@ -1,85 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id$ *)
-
-(***********************************************************************
-  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.
-Unset Boxed Definitions.
-
-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 in |- *; 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/contrib/ring/Setoid_ring.v b/contrib/ring/Setoid_ring.v
index b5cd6b1d0c..93b9bc7cf5 100644
--- a/contrib/ring/Setoid_ring.v
+++ b/contrib/ring/Setoid_ring.v
@@ -10,4 +10,5 @@
 
 Require Export Setoid_ring_theory.
 Require Export Quote.
-Require Export Setoid_ring_normalize.
\ No newline at end of file
+Require Export Setoid_ring_normalize.
+Declare ML Module "ring_plugin".
diff --git a/contrib/ring/g_quote.ml4 b/contrib/ring/g_quote.ml4
deleted file mode 100644
index 808cbbf274..0000000000
--- a/contrib/ring/g_quote.ml4
+++ /dev/null
@@ -1,18 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i camlp4deps: "parsing/grammar.cma" i*)
-
-(* $Id$ *)
-
-open Quote
-
-TACTIC EXTEND quote
-  [ "quote" ident(f) ] -> [ quote f [] ]
-| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ]
-END
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
deleted file mode 100644
index 3b13283e13..0000000000
--- a/contrib/ring/quote.ml
+++ /dev/null
@@ -1,491 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id$ *)
-
-(* The `Quote' tactic *)
-
-(* The basic idea is to automatize the inversion of interpetation 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 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 variables 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 of 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
-     variables 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 map 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 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 variables counter and add an entry to the hashtable; then
-      return \texttt{(Cvar !variables\_counter)}
-   \end{itemize}
-*)
-
-
-(*i*) 
-open Pp
-open Util
-open Names
-open Term
-open Pattern
-open Matching
-open Tacmach
-open Tactics
-open Proof_trees
-open Tacexpr
-(*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 = Coqlib.gen_constant "Quote" ("ring"::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] :=
-     Cases f of
-     | (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{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(
-  struct 
-    type t = constr
-    let compare = (Pervasives.compare : t->t->int)
-  end)
-
-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 () = error "Quote: not a simple fixpoint"
-
-let decomp_term c = kind_of_term (strip_outer_cast 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 = string_of_id 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 typ i nargsi =
-  match kind_of_term typ with
-    | Ind(sp,0) -> 
-        let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in
-        mkApp (mkConstruct ((sp,0),i+1), 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 bodyi index_of_f =
-  let rec aux c = 
-    match kind_of_term c with
-      | App (j, args) when j = mkRel (index_of_f) (* recursive call *) -> 
-          let i = destRel (array_last args) in 
-	  PMeta (Some (coerce_meta_in i))
-      | App (f,args) ->
-          PApp (pattern_of_constr f, Array.map aux args)
-      | Cast (c,_,_) -> aux c 
-      | _ -> pattern_of_constr c
-  in
-  aux bodyi
-
-(*s Now the function [compute_ivs] itself *)
-
-let compute_ivs gl f cs =
-  let cst = try destConst f with _ -> i_can't_do_that () in
-  let body = Environ.constant_value (Global.env()) cst in
-  match decomp_term body with
-    | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
-        let (args3, body3) = decompose_lam body2 in
-        let nargs3 = List.length args3 in
-        begin match decomp_term 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 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 bodyi = mkRel 1 then 
-                     c_lhs := Some (compute_lhs (snd (List.hd args3))
-                                      i nargsi)
-           (* Then we test if the RHS is the RHS for variables *)
-                   else begin match decompose_app bodyi with 
-                     | vmf, [_; _; a3; a4 ]
-                         when isRel a3 & isRel a4 &
-			   pf_conv_x gl vmf 
-                           (Lazy.force coq_varmap_find)->
-                             v_lhs := Some (compute_lhs 
-                                              (snd (List.hd args3))
-                                              i nargsi)
-           (* Third case: this is a normal LHS-RHS *)
-                     | _ -> 
-                         n_lhs_rhs :=
-                         (compute_lhs (snd (List.hd args3)) i nargsi,
-                          compute_rhs bodyi (nargs3 + nargsi + 1))
-                         :: !n_lhs_rhs
-                   end) 
-                lci;
-	      
-              if !c_lhs = None & !v_lhs = None then i_can't_do_that ();
-
-	      (* The Cases predicate is a lambda; we assume no dependency *)
-	      let p = match kind_of_term 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 cset t =
-  (ConstrSet.mem t cset) or
-  (match (kind_of_term t) with
-     | Cast(c,_,_) -> closed_under cset c  
-     | App(f,l) -> closed_under cset f && array_for_all (closed_under 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 n=1 then [] 
-    else (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') or
-  (match (kind_of_term 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 rec insert c = function
-    | [] -> [c]
-    | (h::t as l) when 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)
-
-(*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 ivs lc gl =
-  Coqlib.check_required_library ["Coq";"ring";"Quote"];
-  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.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 = matches rhs c in
-              let s2 = List.map (fun (i,c_i) -> (coerce_meta_out i,aux c_i)) s1
-	      in
-              Termops.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 -> Termops.subst_meta [1, c] c_lhs
-                     | None -> anomaly "invalid inversion scheme for quote"
-                   end
-               | Some var_lhs -> 
-                   begin match ivs.constant_lhs with
-                     | Some c_lhs when closed_under ivs.constants c ->
-			 Termops.subst_meta [1, c] c_lhs
-                     | _ -> 
-			 begin 
-                           try Hashtbl.find varhash c 
-                           with Not_found -> 
-                             let newvar = 
-                               Termops.subst_meta [1, (path_of_int !counter)] 
-				 var_lhs in
-                             begin 
-                               incr counter;
-                               varlist := c :: !varlist;
-                               Hashtbl.add varhash 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 the 
-  conclusion of current goal. Ring for example needs that, but Ring doesn't
-  uses Quote yet. *)
- 
-let quote f lid gl =
-  let f = pf_global gl f in
-  let cl = List.map (pf_global gl) lid in
-  let ivs = compute_ivs gl f cl in
-  let (p, vm) = match quote_terms ivs [(pf_concl gl)] gl with
-    | [p], vm -> (p,vm)
-    | _ -> assert false
-  in
-  match ivs.variable_lhs with
-    | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl
-    | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl
-
-(*i 
-
-Just testing ...
-
-#use "include.ml";;
-open Quote;;
-
-let r = raw_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/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 92f74d1d94..bb6aaea7de 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -752,7 +752,7 @@ let constants_to_unfold =
       "Coq.ring.Ring_normalize.interp_vl";
       "Coq.ring.Ring_abstract.interp_acs";
       "Coq.ring.Ring_abstract.interp_sacs";
-      "Coq.ring.Quote.varmap_find";
+      "Coq.quote.Quote.varmap_find";
       (* anciennement des Local devenus Definition *)
       "Coq.ring.Ring_normalize.ics_aux";
       "Coq.ring.Ring_normalize.ivl_aux";