From 7049e66c2e881dd09092c9360c9db9202be41c63 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 12 Sep 2013 20:51:59 +0000
Subject: 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
---
 pretyping/recordops.ml | 44 --------------------------------------------
 1 file changed, 44 deletions(-)

(limited to 'pretyping/recordops.ml')

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 5aced6e10..eaf7bf0aa 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  *)
-- 
cgit v1.2.3