DISCLAIMER

==========

This big patch is commited here with a HUGE experimental tag on it. It
is probably not a finished job. The aim of committing it now, as
agreed with Hugo, is to get some feedback from potential users to
identify more clearly the directions the implementation could take. So
please feel free to mail me any remarks, bug reports or advices at
<puech@cs.unibo.it>.

Here are the changes induced by it :

For the user
============

* Search tools have been reimplemented to be faster and more
  general. Affected are [SearchPattern], [SearchRewrite] and [Search]
  (not [SearchAbout] yet). Changes are:

  - All of them accept general constructions, and previous syntactical
    limitations are abolished. In particular, one can for example
    [SearchPattern (nat -> Prop)], which will find [isSucc], but also
    [le], [gt] etc.

  - Patterns are typed. This means that you cannot search mistyped
    expressions anymore. I'm not sure if it's a good or a bad thing
    though (especially regarding coercions)...

* New tool to automatically infer (some) Record/Typeclasses instances.
  Usage : [Record/Class *Infer* X := ...] flags a record/class as
  subject to instance search. There is also an option to
  activate/deactivate the search [Set/Unset Autoinstance].  It works
  by finding combinations of definitions (actually all kinds of
  objects) which forms a record instance, possibly parameterized. It
  is activated at two moments:

  - A complete search is done when defining a new record, to find all
    possible instances that could have been formed with past
    definitions. Example: 

      Require Import List.
      Record Infer Monoid A (op:A->A->A) e := 
        { assoc : forall x y z, op x (op y z) = op (op x y) z; 
          idl : forall x, x = op x e ; 
          idr : forall x, x = op e x }.

      new instance Monoid_autoinstance_1 : (Monoid nat plus 0)
      [...]

  - At each new declaration (Definition, Axiom, Inductive), a search
    is made to find instances involving the new object. Example:

      Parameter app_nil_beg : forall A (l:list A), l = nil ++ l.

      new instance Build_Monoid_autoinstance_12 :
      (forall H : Type, Monoid (list H) app nil) :=
      (fun H : Type =>
      Build_Monoid (list H) app nil ass_app (app_nil_beg H)
      (app_nil_end H))


For the developper
==================

* New yet-to-be-named datastructure in [lib/dnet.ml]. Should do
  efficient one-to-many or many-to-one non-linear first-order
  filtering, faster than traditional methods like discrimination nets
  (so yes, the name of the file should probably be changed).

* Comes with its application to Coq's terms
  [pretyping/term_dnet.ml]. Terms are represented so that you can
  search for patterns under products as fast as you would do not under
  products, and facilities are provided to express other kind of
  searches (head of application, under equality, whatever you need
  that can be expressed as a pattern)

* A global repository of all objects defined and imported is
  maintained [toplevel/libtypes.ml], with all search facilities
  described before.

* A certain kind of proof search in [toplevel/autoinstance.ml]. For
  the moment it is specialized on finding instances, but it should be
  generalizable and reusable (more on this in a few months :-).


The bad news
============

* Compile time should increase by 0 to 15% (depending on the size of
  the Requires done). This could be optimized greatly by not
  performing substitutions on modules which are not functors I
  think. There may also be some inefficiency sources left in my code
  though...

* Vo's also gain a little bit of weight (20%). That's inevitable if I
  wanted to store the big datastructure of objects, but could also be
  optimized some more.


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

11 files changed, 853 insertions, 42 deletions

diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
new file mode 100644
index 0000000000..8a9646a174
--- /dev/null
+++ b/toplevel/autoinstance.ml
@@ -0,0 +1,316 @@
+(************************************************************************)
+(*  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:$ *)
+
+(*i*)
+open Pp
+open Printer
+open Names
+open Term
+open Evd
+open Sign
+open Libnames
+(*i*)
+
+(*s 
+ * Automatic detection of (some) record instances
+ *)
+
+(* Datatype for wannabe-instances: a signature is a typeclass along
+   with the collection of evars corresponding to the parameters/fields
+   of the class. Each evar can be uninstantiated (we're still looking
+   for them) or defined (the instance for the field is fixed) *)
+type signature = global_reference * evar list * evar_map
+
+type instance_decl_function = global_reference -> rel_context -> constr list -> unit
+
+(* 
+ * Search algorithm
+ *) 
+
+let rec subst_evar evar def n c = 
+  match kind_of_term c with
+    | Evar (e,_) when e=evar -> lift n def
+    | _ -> map_constr_with_binders (fun n->n+1) (subst_evar evar def) n c
+
+let subst_evar_in_evm evar def evm = 
+  Evd.fold
+    (fun ev evi acc -> 
+       let evar_body = match evi.evar_body with 
+	 | Evd.Evar_empty -> Evd.Evar_empty
+	 | Evd.Evar_defined c -> Evd.Evar_defined (subst_evar evar def 0 c) in
+       let evar_concl = subst_evar evar def 0 evi.evar_concl in
+       Evd.add acc ev {evi with evar_body=evar_body; evar_concl=evar_concl}
+    ) evm empty
+    
+(* Tries to define ev by c in evd. Fails if ev := c1 and c1 /= c ev :
+ * T1, c : T2 and T1 /= T2. Defines recursively all evars instantiated
+ * by this definition. *)
+
+let rec safe_evar_define evm ev c =
+  if not (closedn (-1) c) then raise Termops.CannotFilter else
+(*  msgnl(str"safe_evar_define "++pr_evar_map evm++spc()++str" |- ?"++Util.pr_int ev++str" := "++pr_constr c);*)
+  let evi = (Evd.find evm ev) in
+  let define_subst evm sigma =
+    Util.Intmap.fold
+      ( fun ev (e,c) evm -> 
+	  match kind_of_term c with Evar (i,_) when i=ev -> evm | _ ->
+	    safe_evar_define evm ev (lift (-List.length e) c)
+      ) sigma evm in
+  match evi.evar_body with
+    | Evd.Evar_defined def ->
+	define_subst evm (Termops.filtering [] Reduction.CUMUL def c)
+    | Evd.Evar_empty ->
+	let t = Libtypes.reduce (Typing.type_of (Global.env()) evm c) in
+	let u = Libtypes.reduce (evar_concl evi) in
+	let evm = subst_evar_in_evm ev c evm in
+	define_subst (Evd.define evm ev c) (Termops.filtering [] Reduction.CUMUL t u)
+
+let add_gen_ctx (cl,gen,evm) ctx : signature * constr list = 
+  let rec really_new_evar () =
+    let ev = Evarutil.new_untyped_evar() in
+    if Evd.is_evar evm ev then really_new_evar() else ev in
+  let add_gen_evar (cl,gen,evm) ev ty : signature =
+    let evm = Evd.add evm ev (Evd.make_evar Environ.empty_named_context_val ty) in
+    (cl,ev::gen,evm) in
+  let rec mksubst b = function
+    | [] -> []
+    | a::tl -> b::(mksubst (a::b) tl) in
+  let evl = List.map (fun _ -> really_new_evar()) ctx in
+  let evcl = List.map (fun i -> mkEvar (i,[||])) evl in
+  let substl = List.rev (mksubst [] (evcl)) in
+  let ctx = List.map2 (fun s t -> substnl s 0 t) substl ctx in
+  let sign = List.fold_left2 add_gen_evar (cl,gen,evm) (List.rev evl) ctx in
+  sign,evcl
+
+(* TODO : for full proof-irrelevance in the search, provide a real
+   compare function for constr instead of Pervasive's one! *)
+module SubstSet : Set.S with type elt = Termops.subst
+  = Set.Make (struct type t = Termops.subst
+		     let compare = Util.Intmap.compare (Pervasives.compare)
+	      end)
+
+(* searches instatiations in the library for just one evar [ev] of a
+   signature. [k] is called on each resulting signature *)
+let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) =
+  let ev_typ = Libtypes.reduce (evar_concl evi) in
+  let sort_is_prop = is_Prop (Typing.type_of (Global.env()) evm (evar_concl evi)) in
+(*  msgnl(str"cherche "++pr_constr ev_typ++str" pour "++Util.pr_int ev);*)
+  let substs = ref SubstSet.empty in
+  try List.iter
+    ( fun (gr,(pat,_),s) -> 
+	let (_,genl,_) = Termops.decompose_prod_letin pat in
+	let genl = List.map (fun (_,_,t) -> t) genl in
+	let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) genl in
+	let def = applistc (Libnames.constr_of_global gr) argl in
+(*	msgnl(str"essayons  ?"++Util.pr_int ev++spc()++str":="++spc()
+	      ++pr_constr def++spc()++str":"++spc()++pr_constr (Global.type_of_global gr)*)
+	(*++spc()++str"dans"++spc()++pr_evar_map evm++spc());*)
+	try
+ 	  let evm = safe_evar_define evm ev def in
+	  k (cl,gen,evm);
+	  if sort_is_prop && SubstSet.mem s !substs then raise Exit;
+	  substs := SubstSet.add s !substs
+	with Termops.CannotFilter -> ()
+    ) (Libtypes.search_concl ev_typ)
+  with Exit -> ()
+
+let evm_fold_rev f evm acc =
+  let l = Evd.fold (fun ev evi acc -> (ev,evi)::acc) evm [] in
+  List.fold_left (fun acc (ev,evi) -> f ev evi acc) acc l
+
+exception Continue of Evd.evar * Evd.evar_info
+
+(* searches matches for all the uninstantiated evars of evd in the
+   context. For each totally instantiated evar_map found, apply
+   k. *)
+let rec complete_signature (k:signature -> unit) (cl,gen,evm:signature) =
+  try
+    evm_fold_rev
+      ( fun ev evi _ ->
+	  if not (is_defined evm ev) && not (List.mem ev gen) then
+	    raise (Continue (ev,evi))
+      ) evm (); k (cl,gen,evm)
+  with Continue (ev,evi) -> complete_evar (cl,gen,evm) (ev,evi) (complete_signature k)
+
+(* define all permutations of the evars to evd and call k on the
+   resulting evd *)
+let complete_with_evars_permut (cl,gen,evm:signature) evl c (k:signature -> unit) : unit =
+  let rec aux evm = List.iter
+    ( fun (ctx,ev) ->
+	let tyl = List.map (fun (_,_,t) -> t) ctx in
+	let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) tyl in
+	let def = applistc c argl in	
+(*	msgnl(str"trouvé def ?"++Util.pr_int ev++str" := "++pr_constr def++str " dans "++pr_evar_map evm);*)
+	try
+	  if not (Evd.is_defined evm ev) then
+	    let evm = safe_evar_define evm ev def in
+	    aux evm; k (cl,gen,evm)
+	with Termops.CannotFilter -> ()
+    ) evl in
+  aux evm
+    
+let new_inst_no = 
+  let cnt = ref 0 in
+  fun () -> incr cnt; string_of_int !cnt
+
+let make_instance_ident gr =
+  Nameops.add_suffix (Nametab.id_of_global gr) ("_autoinstance_"^new_inst_no())
+
+let new_instance_message ident typ def =
+  Flags.if_verbose
+  msgnl (str"new instance"++spc()
+	 ++Nameops.pr_id ident++spc()++str":"++spc()
+	 ++pr_constr typ++spc()++str":="++spc()
+	 ++pr_constr def)
+
+open Entries
+
+let rec deep_refresh_universes c = 
+  match kind_of_term c with
+    | Sort (Type _) -> Termops.new_Type()
+    | _ -> map_constr deep_refresh_universes c
+
+let declare_record_instance gr ctx params =
+  let ident = make_instance_ident gr in
+  let def = it_mkLambda_or_LetIn (applistc (constr_of_global gr) params) ctx in
+  let def = deep_refresh_universes def in
+  let ce = { const_entry_body=def; const_entry_type=None;
+	     const_entry_opaque=false; const_entry_boxed=false } in 
+  let cst = Declare.declare_constant ident 
+    (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in
+  new_instance_message ident (Typeops.type_of_constant (Global.env()) cst) def
+
+let declare_class_instance gr ctx params = 
+  let ident = make_instance_ident gr in
+  let cl = Typeclasses.class_info gr in
+  let (def,typ) = Typeclasses.instance_constructor cl params in
+  let (def,typ) = it_mkLambda_or_LetIn def ctx, it_mkProd_or_LetIn typ ctx in
+  let def = deep_refresh_universes def in
+  let typ = deep_refresh_universes typ in
+  let ce = Entries.DefinitionEntry 
+    {  const_entry_type=Some typ; const_entry_body=def;
+       const_entry_opaque=false; const_entry_boxed=false } in 
+  try
+  let cst = Declare.declare_constant ident 
+    (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in
+  Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true cst);
+  new_instance_message ident typ def
+  with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str"  "++Cerrors.explain_exn e)
+
+let rec iter_under_prod (f:rel_context->constr->unit) (ctx:rel_context) t = f ctx t;
+  match kind_of_term t with
+    | Prod (n,t,c) -> iter_under_prod f ((n,None,t)::ctx) c
+    | _ -> ()
+
+(* main search function: search for total instances containing gr, and
+   apply k to each of them *)
+let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature -> unit) : unit =
+  let gr_c = Libnames.constr_of_global gr in
+  let (smap:(Libnames.global_reference * Evd.evar_map,
+   ('a * 'b * Term.constr) list * Evd.evar)
+  Gmapl.t ref) = ref Gmapl.empty in
+  iter_under_prod
+    ( fun ctx typ -> 
+	List.iter
+	  (fun ((cl,ev,evm),_,_) -> 
+(*	     msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_map evm);*)
+	     smap := Gmapl.add (cl,evm) (ctx,ev) !smap)
+	  (Recordops.methods_matching typ)
+    ) [] deftyp;
+  Gmapl.iter 
+    ( fun (cl,evm) evl -> 
+	let f = if Typeclasses.is_class cl then 
+	  declare_class_instance else declare_record_instance in
+	complete_with_evars_permut (cl,[],evm) evl gr_c
+	  (fun sign -> complete_signature (k f) sign)
+    ) !smap
+
+(*
+ * Interface with other parts: hooks & declaration
+ *)
+
+
+let evar_definition evi = match evar_body evi with
+    Evar_empty -> assert false | Evar_defined c -> c
+ 
+let gen_sort_topo l evm = 
+  let iter_evar f ev =
+    let rec aux c = match kind_of_term c with
+	Evar (e,_) -> f e
+      | _ -> iter_constr aux c in
+    aux (Evd.evar_concl (Evd.find evm ev));
+    if Evd.is_defined evm ev then aux (evar_definition (Evd.find evm ev)) in
+  let r = ref [] in 
+  let rec dfs ev = iter_evar dfs ev;
+    if not(List.mem ev !r) then r := ev::!r in
+  List.iter dfs l; List.rev !r
+
+(* register real typeclass instance given a totally defined evd *)
+let declare_instance (k:global_reference -> rel_context -> constr list -> unit)
+    (cl,gen,evm:signature) =
+  let evm = Evarutil.nf_evars evm in
+  let gen = gen_sort_topo gen evm in
+  let (evm,gen) = List.fold_right
+    (fun ev (evm,gen) -> 
+       if Evd.is_defined evm ev 
+       then Evd.remove evm ev,gen 
+       else evm,(ev::gen))
+    gen (evm,[]) in
+(*  msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_map evm);*)
+  let ngen = List.length gen in
+  let (_,ctx,evm) = List.fold_left
+    ( fun (i,ctx,evm) ev -> 
+	let ctx = (Anonymous,None,lift (-i) (Evd.evar_concl(Evd.find evm ev)))::ctx in
+	let evm = subst_evar_in_evm ev (mkRel i) (Evd.remove evm ev) in
+	(i-1,ctx,evm)
+    ) (ngen,[],evm) gen in
+  let fields = List.rev (Evd.fold ( fun ev evi l -> evar_definition evi::l ) evm []) in
+  k cl ctx fields
+
+let autoinstance_opt = ref true
+
+let search_declaration gr =
+  if !autoinstance_opt && 
+    not (Lib.is_modtype()) then
+    let deftyp = Global.type_of_global gr in
+    complete_signature_with_def gr deftyp declare_instance
+
+let search_record k cons sign =
+  if !autoinstance_opt && not (Lib.is_modtype()) then
+    complete_signature (declare_instance k) (cons,[],sign)
+
+(*
+let dh_key = Profile.declare_profile "declaration_hook"
+let ch_key = Profile.declare_profile "class_decl_hook"
+let declaration_hook = Profile.profile1 dh_key declaration_hook
+let class_decl_hook = Profile.profile1 ch_key class_decl_hook
+*)
+
+(*
+ *  Options and bookeeping
+ *)
+
+let begin_autoinstance () =
+  if not !autoinstance_opt then (
+    autoinstance_opt := true;
+  )
+    
+let end_autoinstance () =
+  if !autoinstance_opt then (
+    autoinstance_opt := false;
+ )
+
+let _ =
+  Goptions.declare_bool_option
+    { Goptions.optsync=true;
+      Goptions.optkey=Goptions.PrimaryTable("Autoinstance");
+      Goptions.optname="automatic typeclass instance recognition";
+      Goptions.optread=(fun () -> !autoinstance_opt);
+      Goptions.optwrite=(fun b -> if b then begin_autoinstance() else end_autoinstance()) }
diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli
new file mode 100644
index 0000000000..3866fff39f
--- /dev/null
+++ b/toplevel/autoinstance.mli
@@ -0,0 +1,38 @@
+(************************************************************************)
+(*  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:$ *)
+
+(*i*)
+open Term
+open Libnames
+open Typeclasses
+open Names
+open Evd
+open Sign
+(*i*)
+
+(*s Automatic detection of (some) record instances *)
+
+(* What to do if we find an instance. Passed are : the reference
+ * representing the record/class (definition or constructor) *)
+type instance_decl_function = global_reference -> rel_context -> constr list -> unit
+
+(* [search_declaration gr] Search in the library if the (new)
+ * declaration gr can form an instance of a registered record/class *)
+val search_declaration : global_reference -> unit
+
+(* [search_record declf gr evm] Search the library for instances of
+   the (new) record/class declaration [gr], and register them using
+   [declf]. [evm] is the signature of the record (to avoid recomputing
+   it) *)
+val search_record : instance_decl_function -> global_reference -> evar_map -> unit
+
+(* Instance declaration for both scenarios *)
+val declare_record_instance : instance_decl_function
+val declare_class_instance : instance_decl_function
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 8d480ef2f2..89739b9840 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -143,6 +143,7 @@ let declare_global_definition ident ce local imps =
     if local = Local && Flags.is_verbose() then
       msg_warning (pr_id ident ++ str" is declared as a global definition");
     definition_message ident;
+    Autoinstance.search_declaration (ConstRef kn);
     gr
 
 let declare_definition_hook = ref ignore
@@ -198,6 +199,7 @@ let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) =
         if local=Local & Flags.is_verbose () then
           msg_warning (pr_id ident ++ str" is declared as a parameter" ++
           str" because it is at a global level");
+	Autoinstance.search_declaration (ConstRef kn);
         gr in
   if is_coe then Class.try_add_new_coercion r local
 
@@ -374,6 +376,7 @@ let save id const do_guard (locality,kind) hook =
 	(Local, VarRef id)
     | Local | Global ->
         let kn = declare_constant id (DefinitionEntry const, k) in
+	Autoinstance.search_declaration (ConstRef kn);
 	(Global, ConstRef kn) in
   Pfedit.delete_current_proof ();
   definition_message id;
@@ -644,9 +647,11 @@ let declare_mutual_with_eliminations isrecord mie impls =
   let (_,kn) = declare_mind isrecord mie in    
     list_iter_i (fun i (indimpls, constrimpls) -> 
       let ind = (kn,i) in
+        Autoinstance.search_declaration (IndRef ind);
 	maybe_declare_manual_implicits false (IndRef ind) indimpls;
 	list_iter_i
 	  (fun j impls -> 
+(*	    Autoinstance.search_declaration (ConstructRef (ind,j));*)
 	    maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls)
 	  constrimpls)
       impls;
@@ -802,8 +807,9 @@ let declare_fix boxed kind f def t imps =
   } in
   let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
   let gr = ConstRef kn in
-    maybe_declare_manual_implicits false gr imps;
-    gr
+  Autoinstance.search_declaration (ConstRef kn);
+  maybe_declare_manual_implicits false gr imps;
+  gr
       
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
@@ -1260,4 +1266,3 @@ let get_current_context () =
   with e when Logic.catchable_exception e -> 
     (Evd.empty, Global.env())
 
-
diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml
new file mode 100644
index 0000000000..6fd49b15b9
--- /dev/null
+++ b/toplevel/libtypes.ml
@@ -0,0 +1,109 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+open Term
+open Summary
+open Libobject
+
+(* 
+ * Module construction
+ *)
+  
+let reduce c = Reductionops.head_unfold_under_prod 
+  (Auto.Hint_db.transparent_state (Auto.searchtable_map "typeclass_instances"))
+  (Global.env()) Evd.empty c
+
+module TypeDnet = Term_dnet.Make(struct 
+				   type t = Libnames.global_reference
+				   let compare = Pervasives.compare
+				   let subst s gr = fst (Libnames.subst_global s gr)
+				   let constr_of = Global.type_of_global
+				 end)
+  (struct let reduce = reduce 
+	  let direction = false end)
+
+type result = Libnames.global_reference * (constr*existential_key) * Termops.subst
+
+let all_types = ref TypeDnet.empty
+let defined_types = ref TypeDnet.empty
+
+(*
+ * Bookeeping & States
+ *)
+
+let freeze () = 
+  (!all_types,!defined_types)
+
+let unfreeze (lt,dt) = 
+  all_types := lt; 
+  defined_types := dt
+
+let init () = 
+  all_types := TypeDnet.empty; 
+  defined_types := TypeDnet.empty
+
+let _ = 
+  declare_summary "type-library-state"
+    { freeze_function = freeze;
+      unfreeze_function = unfreeze;
+      init_function = init;
+      survive_module = false;
+      survive_section = false }
+
+let load (_,d) =
+(*  Profile.print_logical_stats !all_types;
+  Profile.print_logical_stats d;*)
+  all_types := TypeDnet.union d !all_types 
+
+let subst s t = TypeDnet.subst s t
+(*
+let subst_key = Profile.declare_profile "subst"
+let subst a b = Profile.profile2 subst_key TypeDnet.subst a b
+
+let load_key = Profile.declare_profile "load"
+let load a = Profile.profile1 load_key load a
+*)
+let (input,output) = 
+  declare_object
+    { (default_object "LIBTYPES") with
+	load_function = (fun _ -> load);
+	subst_function = (fun (_,s,t) -> subst s t);
+	export_function = (fun x -> Some x);
+	classify_function = (fun (_,x) -> Substitute x) 
+    }
+
+let update () = Lib.add_anonymous_leaf (input !defined_types)
+
+(* 
+ * Search interface
+ *)
+
+let search_pattern pat = TypeDnet.search_pattern !all_types pat
+let search_concl pat = TypeDnet.search_concl !all_types pat
+let search_head_concl pat = TypeDnet.search_head_concl !all_types pat
+let search_eq_concl eq pat = TypeDnet.search_eq_concl !all_types eq pat
+
+let add typ gr =
+  defined_types := TypeDnet.add typ gr !defined_types;
+  all_types := TypeDnet.add typ gr !all_types
+(*
+let add_key = Profile.declare_profile "add"
+let add a b = Profile.profile1 add_key add a b
+*)
+    
+(* 
+ * Hooks declaration 
+ *)
+
+let _ = Declare.add_cache_hook 
+  ( fun sp ->
+      let gr = Nametab.absolute_reference sp in
+      let ty = Global.type_of_global gr in
+      add ty gr )
+
+let _ = Declaremods.set_end_library_hook update
diff --git a/toplevel/libtypes.mli b/toplevel/libtypes.mli
new file mode 100644
index 0000000000..be5e9312a2
--- /dev/null
+++ b/toplevel/libtypes.mli
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*  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:$ *)
+
+(*i*)
+open Term
+(*i*)
+
+(* 
+ * Persistent library of all declared object, 
+ * indexed by their types (uses Dnets)
+ *)
+
+(* results are the reference of the object, together with a context
+(constr+evar) and a substitution under this context *)
+type result = Libnames.global_reference * (constr*existential_key) * Termops.subst
+
+(* this is the reduction function used in the indexing process *)
+val reduce : types -> types
+
+(* The different types of search available. 
+ * See term_dnet.mli for more explanations *)
+val search_pattern : types -> result list
+val search_concl : types -> result list
+val search_head_concl : types -> result list
+val search_eq_concl : constr -> types -> result list
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 9978d7bf6d..3ef7eccad9 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -222,8 +222,24 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
       (List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)
 
-let declare_structure finite id idbuild paramimpls params arity fieldimpls fields
-    ?(kind=StructureComponent) ?name is_coe coers =
+let structure_signature ctx =
+  let rec deps_to_evar evm l = 
+    match l with [] -> Evd.empty
+      | [(_,_,typ)] -> Evd.add evm (Evarutil.new_untyped_evar()) 
+	  (Evd.make_evar Environ.empty_named_context_val typ)
+      | (_,_,typ)::tl -> 
+	  let ev = Evarutil.new_untyped_evar() in
+	  let evm = Evd.add evm ev (Evd.make_evar Environ.empty_named_context_val typ) in
+	  let new_tl = Util.list_map_i 
+	    (fun pos (n,c,t) -> n,c,
+	       Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) 1 tl in
+	  deps_to_evar evm new_tl in
+  deps_to_evar Evd.empty (List.rev ctx)
+
+open Typeclasses
+
+let declare_structure finite infer id idbuild paramimpls params arity fieldimpls fields 
+    ?(kind=StructureComponent) ?name is_coe coers sign =
   let nparams = List.length params and nfields = List.length fields in
   let args = extended_rel_list nfields params in
   let ind = applist (mkRel (1+nparams+nfields), args) in
@@ -241,11 +257,14 @@ let declare_structure finite id idbuild paramimpls params arity fieldimpls field
       mind_entry_inds = [mie_ind] } in
   let kn = Command.declare_mutual_with_eliminations true mie [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
+  let cstr = (rsp,1) in
   let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
-  let build = ConstructRef (rsp,1) in
-    if is_coe then Class.try_add_new_coercion build Global;
-    Recordops.declare_structure(rsp,(rsp,1),List.rev kinds,List.rev sp_projs);
-    kn,0
+  let build = ConstructRef cstr in
+  if is_coe then Class.try_add_new_coercion build Global;
+  Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs);
+  if infer then
+    Evd.fold (fun ev evi () -> Recordops.declare_method (ConstructRef cstr) ev sign) sign ();
+  rsp
 
 let implicits_of_context ctx =
   list_map_i (fun i name ->
@@ -256,8 +275,6 @@ let implicits_of_context ctx =
     in ExplByPos (i, explname), (true, true))
     1 (List.rev (Anonymous :: (List.map pi1 ctx)))
 
-open Typeclasses
-
 let typeclasses_db = "typeclass_instances"
 
 let qualid_of_con c = 
@@ -274,8 +291,8 @@ let declare_instance_cst glob con =
       | Some tc -> add_instance (new_instance tc None glob con)
       | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.")
 
-let declare_class finite def id idbuild paramimpls params arity fieldimpls fields
-    ?(kind=StructureComponent) ?name is_coe coers =
+let declare_class finite def infer id idbuild paramimpls params arity fieldimpls fields
+    ?(kind=StructureComponent) ?name is_coe coers sign =
   let fieldimpls = 
     (* Make the class and all params implicits in the projections *)
     let ctx_impls = implicits_of_context params in
@@ -309,15 +326,16 @@ let declare_class finite def id idbuild paramimpls params arity fieldimpls field
 	  (DefinitionEntry proj_entry, IsDefinition Definition) 
 	in
 	let cref = ConstRef cst in
-	  Impargs.declare_manual_implicits false cref paramimpls;
-	  Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
-	  set_rigid cst; (* set_rigid proj_cst; *)
-	  cref, [proj_name, Some proj_cst]
+	Impargs.declare_manual_implicits false cref paramimpls;
+	Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
+	set_rigid cst; (* set_rigid proj_cst; *)
+	if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign ();
+	cref, [proj_name, Some proj_cst]
     | _ ->
 	let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in
-	let ind = declare_structure true (snd id) idbuild paramimpls
+	let ind = declare_structure true infer (snd id) idbuild paramimpls
 	  params (Option.cata (fun x -> x) (new_Type ()) arity) fieldimpls fields
-	  ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields)
+	  ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign
 	in
 	  (* List.iter (Option.iter (declare_interning_data ((),[]))) notations; *)
 	  IndRef ind, (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y))
@@ -339,7 +357,7 @@ let declare_class finite def id idbuild paramimpls params arity fieldimpls field
     List.iter2 (fun p sub -> 
       if sub then match snd p with Some p -> declare_instance_cst true p | None -> ())
       k.cl_projs coers;
-    add_class k; impl
+  add_class k; impl
 
 let interp_and_check_sort sort =
   Option.map (fun sort ->
@@ -349,10 +367,11 @@ let interp_and_check_sort sort =
     else user_err_loc (constr_loc sort,"", str"Sort expected.")) sort
 
 open Vernacexpr
+open Autoinstance
 
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean 
    list telling if the corresponding fields must me declared as coercion *)
-let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
+let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
   let cfs,notations = List.split cfs in
   let coers,fs = List.split cfs in
   let extract_name acc = function
@@ -365,13 +384,18 @@ let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
   let sc = interp_and_check_sort s in
   let implpars, params, implfs, fields = 
     States.with_heavy_rollback (fun () ->
-      typecheck_params_and_fields idstruc sc ps notations fs) ()
-  in
+      typecheck_params_and_fields idstruc sc ps notations fs) () in
+  let sign = structure_signature (fields@params) in
     match kind with
     | Record | Structure ->
 	let arity = Option.default (new_Type ()) sc in
 	let implfs = List.map
-	  (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs
-	in IndRef (declare_structure finite idstruc idbuild implpars params arity implfs fields is_coe coers)
-    | Class b ->
-	declare_class finite b (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers
+	  (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in
+	let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs fields is_coe coers sign in
+	if infer then search_record declare_record_instance (ConstructRef (ind,1)) sign;
+	IndRef ind	  
+    | Class def ->
+	let gr = declare_class finite def infer (loc,idstruc) idbuild 
+	  implpars params sc implfs fields is_coe coers sign in
+	if infer then search_record declare_class_instance gr sign;
+	gr
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 3fe18e1926..564d4409f0 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -27,15 +27,16 @@ val declare_projections :
   bool list -> manual_explicitation list list -> rel_context -> 
   (name * bool) list * constant option list
 
-val declare_structure : bool (*coinductive?*)-> identifier -> identifier -> 
+val declare_structure : bool (*coinductive?*)-> bool (*infer?*) -> identifier -> identifier -> 
   manual_explicitation list -> rel_context -> (* params *) constr -> (* arity *)
   Impargs.manual_explicitation list list -> rel_context -> (* fields *)
   ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
   bool -> (* coercion? *)
   bool list -> (* field coercions *)
+  Evd.evar_map ->
   inductive
 
 val definition_structure :
-  record_kind * bool (*coinductive?*)*lident with_coercion * local_binder list *
+  record_kind * bool (*coinductive?*) * bool(*infer?*)* lident with_coercion * local_binder list *
   (local_decl_expr with_coercion with_notation) list * 
   identifier * constr_expr option -> global_reference
diff --git a/toplevel/search.ml b/toplevel/search.ml
new file mode 100644
index 0000000000..e50af97332
--- /dev/null
+++ b/toplevel/search.ml
@@ -0,0 +1,232 @@
+(************************************************************************)
+(*  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$ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+open Rawterm
+open Declarations
+open Libobject
+open Declare
+open Environ
+open Pattern
+open Matching
+open Printer
+open Libnames
+open Nametab
+
+(* The functions print_constructors and crible implement the behavior needed
+   for the Coq searching commands.
+   These functions take as first argument the procedure
+   that will be called to treat each entry.  This procedure receives the name
+   of the object, the assumptions that will make it possible to print its type,
+   and the constr term that represent its type. *)
+
+let print_constructors indsp fn env nconstr =
+  for i = 1 to nconstr do
+    fn (ConstructRef (indsp,i)) env (Inductiveops.type_of_constructor env (indsp,i))
+  done
+
+let rec head_const c = match kind_of_term c with
+  | Prod (_,_,d) -> head_const d
+  | LetIn (_,_,_,d) -> head_const d
+  | App (f,_)   -> head_const f
+  | Cast (d,_,_)   -> head_const d
+  | _            -> c
+
+(* General search, restricted to head constant if [only_head] *)
+
+let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
+  let env = Global.env () in
+  let crible_rec (sp,_) lobj = match object_tag lobj with
+    | "VARIABLE" ->
+	(try 
+	   let (id,_,typ) = Global.lookup_named (basename sp) in 
+           if refopt = None
+	     || head_const typ = constr_of_global (Option.get refopt)
+	   then
+	     fn (VarRef id) env typ
+	 with Not_found -> (* we are in a section *) ())
+    | "CONSTANT" ->
+	let cst = locate_constant (qualid_of_sp sp) in
+	let typ = Typeops.type_of_constant env cst in
+        if refopt = None
+	  || head_const typ = constr_of_global (Option.get refopt)
+	then
+	  fn (ConstRef cst) env typ
+    | "INDUCTIVE" -> 
+	let kn = locate_mind (qualid_of_sp sp) in
+        let mib = Global.lookup_mind kn in 
+        (match refopt with 
+	  | Some (IndRef ((kn',tyi) as ind)) when kn=kn' ->
+	      print_constructors ind fn env
+	        (Array.length (mib.mind_packets.(tyi).mind_user_lc))
+          | Some _ -> ()
+	  | _ ->
+              Array.iteri 
+	        (fun i mip -> print_constructors (kn,i) fn env
+	          (Array.length mip.mind_user_lc)) mib.mind_packets)
+    | _ -> ()
+  in 
+  try 
+    Declaremods.iter_all_segments crible_rec
+  with Not_found -> 
+    ()
+
+let crible ref = gen_crible (Some ref)
+
+(* Fine Search. By Yves Bertot. *)
+
+exception No_section_path
+
+let rec head c = 
+  let c = strip_outer_cast c in
+  match kind_of_term c with
+  | Prod (_,_,c) -> head c
+  | LetIn (_,_,_,c) -> head c
+  | _              -> c
+      
+let constr_to_section_path c = match kind_of_term c with
+  | Const sp -> sp
+  | _ -> raise No_section_path
+      
+let xor a b = (a or b) & (not (a & b))
+
+let plain_display ref a c =
+  let pc = pr_lconstr_env a c in
+  let pr = pr_global ref in
+  msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ())
+
+let filter_by_module (module_list:dir_path list) (accept:bool) 
+  (ref:global_reference) _ _ =
+  try
+    let sp = sp_of_global ref in
+    let sl = dirpath sp in
+    let rec filter_aux = function
+      | m :: tl -> (not (is_dirpath_prefix_of m sl)) && (filter_aux tl)
+      | [] -> true 
+    in
+    xor accept (filter_aux module_list)
+  with No_section_path -> 
+    false
+
+let ref_eq = Libnames.encode_kn Coqlib.logic_module (id_of_string "eq"), 0
+let c_eq = mkInd ref_eq
+let gref_eq = IndRef ref_eq
+
+let mk_rewrite_pattern1 eq pattern =
+  PApp (PRef eq, [| PMeta None; pattern; PMeta None |])
+
+let mk_rewrite_pattern2 eq pattern =
+  PApp (PRef eq, [| PMeta None; PMeta None; pattern |])
+
+let pattern_filter pat _ a c =
+  try 
+    try
+      is_matching pat (head c) 
+    with _ -> 
+      is_matching
+	pat (head (Typing.type_of (Global.env()) Evd.empty c))
+    with UserError _ -> 
+      false
+
+let filtered_search filter_function display_function ref =
+  crible ref
+    (fun s a c -> if filter_function s a c then display_function s a c) 
+
+let rec id_from_pattern = function
+  | PRef gr -> gr
+(* should be appear as a PRef (VarRef sp) !!
+  | PVar id -> Nametab.locate (make_qualid [] (string_of_id id))
+ *)
+  | PApp (p,_) -> id_from_pattern p
+  | _ -> error "The pattern is not simple enough."
+	
+let raw_pattern_search extra_filter display_function pat =
+  let name = id_from_pattern pat in
+  filtered_search 
+    (fun s a c -> (pattern_filter pat s a c) & extra_filter s a c) 
+    display_function name
+
+let raw_search_rewrite extra_filter display_function pattern =
+  filtered_search
+    (fun s a c ->
+       ((pattern_filter (mk_rewrite_pattern1 gref_eq pattern) s a c) ||
+        (pattern_filter (mk_rewrite_pattern2 gref_eq pattern) s a c)) 
+       && extra_filter s a c)
+    display_function gref_eq
+
+(* 
+ * functions to use the new Libtypes facility
+ *)
+
+let raw_search search_function extra_filter display_function pat =
+  let env = Global.env() in
+  List.iter 
+    (fun (gr,_,_) -> 
+       let typ = Global.type_of_global gr in
+       if extra_filter gr env typ then
+	 display_function gr env typ
+    ) (search_function pat)
+
+let raw_pattern_search = raw_search Libtypes.search_concl
+let raw_search_rewrite = raw_search (Libtypes.search_eq_concl c_eq)
+let raw_search_by_head = raw_search Libtypes.search_head_concl
+
+let text_pattern_search extra_filter =
+  raw_pattern_search extra_filter plain_display
+
+let text_search_rewrite extra_filter =
+  raw_search_rewrite extra_filter plain_display
+
+let text_search_by_head extra_filter =
+  raw_search_by_head extra_filter plain_display
+
+let filter_by_module_from_list = function
+  | [], _ -> (fun _ _ _ -> true)
+  | l, outside -> filter_by_module l (not outside)
+
+let search_by_head pat inout = 
+  text_search_by_head (filter_by_module_from_list inout) pat
+
+let search_rewrite pat inout =
+  text_search_rewrite (filter_by_module_from_list inout) pat
+
+let search_pattern pat inout =
+  text_pattern_search (filter_by_module_from_list inout) pat
+
+let gen_filtered_search filter_function display_function =
+  gen_crible None
+    (fun s a c -> if filter_function s a c then display_function s a c) 
+
+(** SearchAbout *)
+
+let name_of_reference ref = string_of_id (id_of_global ref)
+
+type glob_search_about_item =
+  | GlobSearchSubPattern of constr_pattern
+  | GlobSearchString of string
+
+let search_about_item (itemref,typ) = function
+  | GlobSearchSubPattern pat -> is_matching_appsubterm ~closed:false pat typ
+  | GlobSearchString s -> string_string_contains (name_of_reference itemref) s
+
+let raw_search_about filter_modules display_function l =
+  let filter ref' env typ =
+    filter_modules ref' env typ &&
+    List.for_all (fun (b,i) -> b = search_about_item (ref',typ) i) l && 
+    not (string_string_contains (name_of_reference ref') "_subproof")
+  in
+  gen_filtered_search filter display_function
+
+let search_about ref inout = 
+  raw_search_about (filter_by_module_from_list inout) plain_display ref
diff --git a/toplevel/search.mli b/toplevel/search.mli
new file mode 100644
index 0000000000..5b978770b0
--- /dev/null
+++ b/toplevel/search.mli
@@ -0,0 +1,52 @@
+(************************************************************************)
+(*  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 $Id$ i*)
+
+open Pp
+open Names
+open Term
+open Environ
+open Pattern
+open Libnames
+open Nametab
+
+(*s Search facilities. *)
+
+type glob_search_about_item =
+  | GlobSearchSubPattern of constr_pattern
+  | GlobSearchString of string
+
+val search_by_head : constr -> dir_path list * bool -> unit
+val search_rewrite : constr -> dir_path list * bool -> unit
+val search_pattern : constr -> dir_path list * bool -> unit
+val search_about  : 
+  (bool * glob_search_about_item) list -> dir_path list * bool -> unit
+
+(* The filtering function that is by standard search facilities.
+   It can be passed as argument to the raw search functions.
+   It is used in pcoq. *)
+
+val filter_by_module_from_list :
+  dir_path list * bool -> global_reference -> env -> 'a -> bool
+
+(* raw search functions can be used for various extensions.
+   They are also used for pcoq. *)
+val gen_filtered_search : (global_reference -> env -> constr -> bool) ->
+      (global_reference -> env -> constr -> unit) -> unit
+val filtered_search : (global_reference -> env -> constr -> bool) -> 
+  (global_reference -> env -> constr -> unit) -> global_reference -> unit
+val raw_pattern_search : (global_reference -> env -> constr -> bool) ->
+  (global_reference -> env -> constr -> unit) -> constr -> unit
+val raw_search_rewrite : (global_reference -> env -> constr -> bool) ->
+  (global_reference -> env -> constr -> unit) -> constr -> unit
+val raw_search_about : (global_reference -> env -> constr -> bool) ->
+  (global_reference -> env -> constr -> unit) -> 
+      (bool * glob_search_about_item) list -> unit
+val raw_search_by_head : (global_reference -> env -> constr -> bool) ->
+  (global_reference -> env -> constr -> unit) -> constr -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a4d3e5458a..37e9cf22ae 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -375,7 +375,7 @@ let vernac_assumption kind l nl=
 	  else Dumpglob.dump_definition lid true "var") idl;
       declare_assumption idl is_coe kind [] c false false nl) l
 	  
-let vernac_record k finite struc binders sort nameopt cfs =
+let vernac_record k finite infer struc binders sort nameopt cfs =
   let const = match nameopt with 
     | None -> add_prefix "Build_" (snd (snd struc))
     | Some (_,id as lid) ->
@@ -386,9 +386,9 @@ let vernac_record k finite struc binders sort nameopt cfs =
 	match x with
 	| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
 	| _ -> ()) cfs);
-    ignore(Record.definition_structure (k,finite,struc,binders,cfs,const,sort))
+    ignore(Record.definition_structure (k,finite,infer,struc,binders,cfs,const,sort))
       
-let vernac_inductive finite indl = 
+let vernac_inductive finite infer indl = 
   if Dumpglob.dump () then
     List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
       match cstrs with 
@@ -401,12 +401,12 @@ let vernac_inductive finite indl =
   match indl with
   | [ ( id , bl , c , Some b, RecordDecl (oc,fs) ), None ] -> 
       vernac_record (match b with Class true -> Class false | _ -> b)
-	finite id bl c oc fs
+	finite infer id bl c oc fs
   | [ ( id , bl , c , Some (Class true), Constructors [l]), _ ] -> 
       let f = 
 	let (coe, ((loc, id), ce)) = l in
 	  ((coe, AssumExpr ((loc, Name id), ce)), None)
-      in vernac_record (Class true) finite id bl c None [f]
+      in vernac_record (Class true) finite infer id bl c None [f]
   | [ ( id , bl , c , Some (Class true), _), _ ] -> 
       Util.error "Definitional classes must have a single method"
   | [ ( id , bl , c , Some (Class false), Constructors _), _ ] ->
@@ -1143,13 +1143,14 @@ let vernac_search s r =
   if !pcoq <> None then (Option.get !pcoq).search s r else
   match s with
   | SearchPattern c ->
-      let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
-      Search.search_pattern pat r
+      let (_,c) = interp_open_constr_patvar Evd.empty (Global.env()) c in
+      Search.search_pattern c r
   | SearchRewrite c ->
-      let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
+      let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in
       Search.search_rewrite pat r
-  | SearchHead ref ->
-      Search.search_by_head (global_with_alias ref) r
+  | SearchHead c ->
+      let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in
+      Search.search_by_head pat r
   | SearchAbout sl ->
       Search.search_about (List.map (on_snd interp_search_about_item) sl) r
 
@@ -1310,7 +1311,7 @@ let interp c = match c with
   | VernacEndProof e -> vernac_end_proof e
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl
-  | VernacInductive (finite,l) -> vernac_inductive finite l
+  | VernacInductive (finite,infer,l) -> vernac_inductive finite infer l
   | VernacFixpoint (l,b) -> vernac_fixpoint l b
   | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b
   | VernacScheme l -> vernac_scheme l
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 5ea0235a5a..9412a5981c 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -75,7 +75,7 @@ type search_about_item =
 type searchable =
   | SearchPattern of constr_pattern_expr
   | SearchRewrite of constr_pattern_expr
-  | SearchHead of reference
+  | SearchHead of constr_pattern_expr
   | SearchAbout of (bool * search_about_item) list
 
 type locatable =
@@ -143,6 +143,7 @@ type export_flag    = bool (* true = Export;        false = Import         *)
 type specif_flag    = bool (* true = Specification; false = Implementation *)
 type inductive_flag = bool (* true = Inductive;     false = CoInductive    *)
 type onlyparsing_flag = bool (* true = Parse only;  false = Print also     *)
+type infer_flag     = bool (* true = try to Infer record; false = nothing  *)
 
 type sort_expr = Rawterm.rawsort
 
@@ -211,7 +212,7 @@ type vernac_expr =
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
   | VernacAssumption of assumption_kind * bool * simple_binder with_coercion list
-  | VernacInductive of inductive_flag * (inductive_expr * decl_notation) list
+  | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation) list
   | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool
   | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool
   | VernacScheme of (lident option * scheme) list