Unplugging Autoinstance. The code is still here if someone wishes

to fix it, but it should be eventually erased.

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

2 files changed, 0 insertions, 53 deletions

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 5aced6e10c..eaf7bf0aa9 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -105,50 +105,6 @@ let find_projection = function
   | ConstRef cst -> Cmap.find cst !projection_table
   | _ -> raise Not_found
 
-(* Management of a field store : each field + argument of the inferred
- * records are stored in a discrimination tree *)
-
-let subst_id s (gr,ev,evm) =
-  (fst(subst_global s gr),ev,Evd.subst_evar_map s evm)
-
-module MethodsDnet : Term_dnet.S
-  with type ident = global_reference * Evd.evar * Evd.evar_map
-  = Term_dnet.Make
-  (struct
-     type t = global_reference * Evd.evar * Evd.evar_map
-     (** ppedrot: FIXME: this is surely wrong, generic equality has nothing to 
-         do w.r.t. evar maps. *)
-     let compare = Pervasives.compare
-     let subst = subst_id
-     let constr_of (_,ev,evm) = Evd.evar_concl (Evd.find evm ev)
-   end)
-  (struct
-     let reduce c = Reductionops.head_unfold_under_prod
-       Names.full_transparent_state (Global.env()) Evd.empty c
-     let direction = true
-   end)
-
-let meth_dnet = Summary.ref MethodsDnet.empty ~name:"record-methods-state"
-
-open Libobject
-
-let load_method (_,(ty,id)) =
-  meth_dnet := MethodsDnet.add ty id !meth_dnet
-
-let in_method : constr * MethodsDnet.ident -> obj =
-  declare_object
-    { (default_object "RECMETHODS") with
-	load_function = (fun _ -> load_method);
-	cache_function = load_method;
-	subst_function = (fun (s,(ty,id)) -> Mod_subst.subst_mps s ty,subst_id s id);
-	classify_function = (fun x -> Substitute x)
-    }
-
-let methods_matching c = MethodsDnet.search_pattern !meth_dnet c
-
-let declare_method cons ev sign =
-  Lib.add_anonymous_leaf (in_method ((Evd.evar_concl (Evd.find sign ev)),(cons,ev,sign)))
-
 (************************************************************************)
 (*s A canonical structure declares "canonical" conversion hints between *)
 (*  the effective components of a structure and the projections of the  *)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 11e558a76d..0623265053 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -45,15 +45,6 @@ val find_projection_nparams : global_reference -> int
 (** raise [Not_found] if not a projection *)
 val find_projection : global_reference -> struc_typ
 
-(** we keep an index (dnet) of record's arguments + fields
-   (=methods). Here is how to declare them: *)
-val declare_method :
-  global_reference -> Evd.evar -> Evd.evar_map -> unit
-  (** and here is how to search for methods matched by a given term: *)
-val methods_matching : constr ->
-  ((global_reference*Evd.evar*Evd.evar_map) *
-     (constr*existential_key)*Termops.subst) list
-
 (** {6 Canonical structures } *)
 (** A canonical structure declares "canonical" conversion hints between 
     the effective components of a structure and the projections of the