SearchPattern et SearchRewrite

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

8 files changed, 306 insertions, 89 deletions

diff --git a/.depend b/.depend
index db13f54aa..65b864af6 100644
--- a/.depend
+++ b/.depend
@@ -71,6 +71,8 @@ parsing/pretty.cmi: kernel/declarations.cmi kernel/environ.cmi \
 parsing/printer.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \
     parsing/pattern.cmi lib/pp.cmi pretyping/rawterm.cmi kernel/sign.cmi \
     kernel/term.cmi 
+parsing/search.cmi: kernel/environ.cmi parsing/pattern.cmi lib/pp.cmi \
+    kernel/term.cmi 
 parsing/termast.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \
     parsing/pattern.cmi pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi 
 pretyping/cases.cmi: kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
@@ -439,6 +441,14 @@ parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \
     parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi 
 parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \
     parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi 
+parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
+    toplevel/vernac.cmi 
+parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
+    toplevel/vernac.cmx 
+parsing/g_cases.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_cases.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
+parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx 
 parsing/g_natsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
     parsing/coqast.cmi parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi \
     lib/pp.cmi lib/util.cmi parsing/g_natsyntax.cmi 
@@ -447,12 +457,24 @@ parsing/g_natsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \
     lib/pp.cmx lib/util.cmx parsing/g_natsyntax.cmi 
 parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernac.cmi 
 parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmx toplevel/vernac.cmx 
+parsing/g_proofs.cmo: parsing/coqast.cmi parsing/pcoq.cmi lib/pp.cmi \
+    lib/util.cmi toplevel/vernac.cmi 
+parsing/g_proofs.cmx: parsing/coqast.cmx parsing/pcoq.cmx lib/pp.cmx \
+    lib/util.cmx toplevel/vernac.cmx 
 parsing/g_rsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
     parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \
     lib/util.cmi 
 parsing/g_rsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
     parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx \
     lib/util.cmx 
+parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
+    lib/pp.cmi lib/util.cmi 
+parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
+    lib/pp.cmx lib/util.cmx 
+parsing/g_vernac.cmo: parsing/coqast.cmi parsing/pcoq.cmi lib/pp.cmi \
+    lib/util.cmi toplevel/vernac.cmi 
+parsing/g_vernac.cmx: parsing/coqast.cmx parsing/pcoq.cmx lib/pp.cmx \
+    lib/util.cmx toplevel/vernac.cmx 
 parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
     parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \
     lib/util.cmi parsing/g_zsyntax.cmi 
@@ -474,17 +496,17 @@ parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \
 parsing/pretty.cmo: pretyping/classops.cmi kernel/declarations.cmi \
     library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
     library/impargs.cmi kernel/inductive.cmi kernel/instantiate.cmi \
-    library/lib.cmi library/libobject.cmi library/library.cmi \
-    kernel/names.cmi lib/pp.cmi parsing/printer.cmi kernel/reduction.cmi \
-    kernel/sign.cmi pretyping/syntax_def.cmi kernel/term.cmi \
-    kernel/typeops.cmi lib/util.cmi parsing/pretty.cmi 
+    library/lib.cmi library/libobject.cmi kernel/names.cmi lib/pp.cmi \
+    parsing/printer.cmi kernel/reduction.cmi kernel/sign.cmi \
+    pretyping/syntax_def.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \
+    parsing/pretty.cmi 
 parsing/pretty.cmx: pretyping/classops.cmx kernel/declarations.cmx \
     library/declare.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \
     library/impargs.cmx kernel/inductive.cmx kernel/instantiate.cmx \
-    library/lib.cmx library/libobject.cmx library/library.cmx \
-    kernel/names.cmx lib/pp.cmx parsing/printer.cmx kernel/reduction.cmx \
-    kernel/sign.cmx pretyping/syntax_def.cmx kernel/term.cmx \
-    kernel/typeops.cmx lib/util.cmx parsing/pretty.cmi 
+    library/lib.cmx library/libobject.cmx kernel/names.cmx lib/pp.cmx \
+    parsing/printer.cmx kernel/reduction.cmx kernel/sign.cmx \
+    pretyping/syntax_def.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \
+    parsing/pretty.cmi 
 parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
     kernel/environ.cmi parsing/esyntax.cmi parsing/extend.cmi \
     library/global.cmi kernel/names.cmi lib/options.cmi parsing/pattern.cmi \
@@ -497,6 +519,18 @@ parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
     lib/util.cmx parsing/printer.cmi 
 parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
 parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
+parsing/search.cmo: parsing/astterm.cmi parsing/coqast.cmi \
+    kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
+    kernel/evd.cmi library/global.cmi library/libobject.cmi \
+    library/library.cmi kernel/names.cmi library/nametab.cmi \
+    parsing/pattern.cmi lib/pp.cmi parsing/pretty.cmi parsing/printer.cmi \
+    kernel/term.cmi pretyping/typing.cmi lib/util.cmi parsing/search.cmi 
+parsing/search.cmx: parsing/astterm.cmx parsing/coqast.cmx \
+    kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \
+    kernel/evd.cmx library/global.cmx library/libobject.cmx \
+    library/library.cmx kernel/names.cmx library/nametab.cmx \
+    parsing/pattern.cmx lib/pp.cmx parsing/pretty.cmx parsing/printer.cmx \
+    kernel/term.cmx pretyping/typing.cmx lib/util.cmx parsing/search.cmi 
 parsing/termast.cmo: parsing/ast.cmi pretyping/classops.cmi \
     parsing/coqast.cmi library/declare.cmi pretyping/detyping.cmi \
     kernel/environ.cmi library/impargs.cmi kernel/inductive.cmi \
@@ -929,6 +963,12 @@ tactics/tactics.cmx: parsing/astterm.cmx proofs/clenv.cmx \
     kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx \
     proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \
     kernel/term.cmx lib/util.cmx tactics/tactics.cmi 
+tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \
+    kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \
+    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi 
+tactics/tauto.cmx: parsing/ast.cmx parsing/coqast.cmx tactics/hipattern.cmx \
+    kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx 
 tactics/termdn.cmo: tactics/dn.cmi kernel/names.cmi parsing/pattern.cmi \
     pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi tactics/termdn.cmi 
 tactics/termdn.cmx: tactics/dn.cmx kernel/names.cmx parsing/pattern.cmx \
@@ -1081,8 +1121,8 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmi \
     kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
     lib/pp.cmx toplevel/protectedtoplevel.cmx lib/util.cmx \
     toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi 
-toplevel/usage.cmo: toplevel/usage.cmi 
-toplevel/usage.cmx: toplevel/usage.cmi 
+toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi 
+toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi 
 toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi \
     toplevel/discharge.cmi library/library.cmi lib/options.cmi \
     parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi library/states.cmi \
@@ -1101,11 +1141,12 @@ toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
     lib/options.cmi proofs/pfedit.cmi lib/pp.cmi lib/pp_control.cmi \
     parsing/pretty.cmi pretyping/pretype_errors.cmi parsing/printer.cmi \
     proofs/proof_trees.cmi proofs/proof_type.cmi toplevel/record.cmi \
-    kernel/reduction.cmi proofs/refiner.cmi lib/stamps.cmi library/states.cmi \
-    pretyping/syntax_def.cmi lib/system.cmi proofs/tacinterp.cmi \
-    proofs/tacmach.cmi pretyping/tacred.cmi proofs/tactic_debug.cmi \
-    tactics/tactics.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \
-    toplevel/vernacinterp.cmi toplevel/vernacentries.cmi 
+    kernel/reduction.cmi proofs/refiner.cmi parsing/search.cmi lib/stamps.cmi \
+    library/states.cmi pretyping/syntax_def.cmi lib/system.cmi \
+    proofs/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
+    proofs/tactic_debug.cmi tactics/tactics.cmi kernel/term.cmi \
+    kernel/typeops.cmi lib/util.cmi toplevel/vernacinterp.cmi \
+    toplevel/vernacentries.cmi 
 toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \
     toplevel/class.cmx toplevel/command.cmx parsing/coqast.cmx \
     library/declare.cmx toplevel/discharge.cmx kernel/environ.cmx \
@@ -1116,11 +1157,12 @@ toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \
     lib/options.cmx proofs/pfedit.cmx lib/pp.cmx lib/pp_control.cmx \
     parsing/pretty.cmx pretyping/pretype_errors.cmx parsing/printer.cmx \
     proofs/proof_trees.cmx proofs/proof_type.cmx toplevel/record.cmx \
-    kernel/reduction.cmx proofs/refiner.cmx lib/stamps.cmx library/states.cmx \
-    pretyping/syntax_def.cmx lib/system.cmx proofs/tacinterp.cmx \
-    proofs/tacmach.cmx pretyping/tacred.cmx proofs/tactic_debug.cmx \
-    tactics/tactics.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \
-    toplevel/vernacinterp.cmx toplevel/vernacentries.cmi 
+    kernel/reduction.cmx proofs/refiner.cmx parsing/search.cmx lib/stamps.cmx \
+    library/states.cmx pretyping/syntax_def.cmx lib/system.cmx \
+    proofs/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
+    proofs/tactic_debug.cmx tactics/tactics.cmx kernel/term.cmx \
+    kernel/typeops.cmx lib/util.cmx toplevel/vernacinterp.cmx \
+    toplevel/vernacentries.cmi 
 toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi \
     toplevel/command.cmi parsing/coqast.cmi lib/dyn.cmi toplevel/himsg.cmi \
     kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
diff --git a/Makefile b/Makefile
index 3c979eaff..4aa74c159 100644
--- a/Makefile
+++ b/Makefile
@@ -91,7 +91,8 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \
 	parsing/g_vernac.cmo parsing/g_proofs.cmo parsing/g_tactic.cmo \
 	parsing/g_constr.cmo parsing/g_cases.cmo \
         parsing/extend.cmo parsing/esyntax.cmo \
-	parsing/printer.cmo parsing/pretty.cmo parsing/egrammar.cmo \
+	parsing/printer.cmo parsing/pretty.cmo parsing/search.cmo \
+        parsing/egrammar.cmo \
         parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo
 
 ARITHSYNTAX=parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo
@@ -192,7 +193,7 @@ clean::
 archclean::
 	rm -f $(COQTOPBYTE) $(COQTOPOPT) $(BESTCOQTOP) $(COQC) $(COQMKTOP)
 
-# we provide targets for each subdirectories
+# we provide targets for each subdirectory
 
 lib: $(LIB)
 kernel: $(KERNEL)
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index d9eaf2a0a..e5ed92ea2 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -97,6 +97,10 @@ GEXTEND Gram
       | IDENT "Print"; id = identarg; "." -> <:ast< (PrintId $id) >>
       | IDENT "Search"; id = Tactic.qualidarg; "." -> <:ast< (SEARCH $id) >>
       | IDENT "Inspect"; n = numarg; "." -> <:ast< (INSPECT $n) >>
+      | IDENT "SearchPattern"; c = constrarg; l = in_or_out_modules; "." ->
+	  <:ast< (SearchPattern $c ($LIST $l)) >>
+      | IDENT "SearchRewrite"; c = constrarg; l = in_or_out_modules; "." ->
+	  <:ast< (SearchRewrite $c ($LIST $l)) >>
       (* TODO: rapprocher Eval et Check *)
       | IDENT "Eval"; r = Tactic.red_tactic; "in"; c = constrarg; "." ->
           <:ast< (Eval (TACTIC_ARG (REDEXP $r)) $c) >>
@@ -186,6 +190,11 @@ GEXTEND Gram
     [ [ IDENT "Check" -> <:ast< "CHECK" >>
       | "Type" -> <:ast< "PRINTTYPE" >> ] ] (* pas dans le RefMan *)
   ;
+  in_or_out_modules:
+    [ [ IDENT "inside"; l = ne_identarg_list -> <:ast< "inside" >> :: l
+      | IDENT "outside"; l = ne_identarg_list -> <:ast< "outside" >> :: l
+      | -> [] ] ]
+  ;
 END;
 
 (* Grammar extensions *)
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index ff1e7275e..7c4c40aa1 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -274,13 +274,6 @@ let print_full_context_typ () = print_context false (Lib.contents_after None)
    assume that the declaration of constructors and eliminations
    follows the definition of the inductive type *)
 
-let rec head_const c = match kind_of_term c with
-  | IsProd (_,_,d) -> head_const d
-  | IsLetIn (_,_,_,d) -> head_const d
-  | IsApp (f,_)   -> head_const f
-  | IsCast (d,_)   -> head_const d
-  | _            -> c
-
 let list_filter_vec f vec = 
   let rec frec n lf = 
     if n < 0 then lf 
@@ -291,62 +284,6 @@ let list_filter_vec f vec =
   in 
   frec (Array.length vec -1) []
 
- (* The functions print_constructors and crible implement the behavior needed
-   for the Coq Search command.
-   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 fn env_ar mip = 
-  let _ =
-    array_map2 (fun id c -> fn (pr_id id) (* il faudrait qualifier... *)
-		    env_ar (body_of_type c))
-    mip.mind_consnames (mind_user_lc mip)
-  in ()
-
-let crible (fn : std_ppcmds -> env -> constr -> unit) ref =
-  let env = Global.env () in
-  let imported = Library.opened_modules() in
-  let const = constr_of_reference Evd.empty env ref in 
-  let crible_rec sp lobj =
-    match object_tag lobj with
-      | "VARIABLE" ->
-	  let ((idc,_,typ),_,_) = get_variable sp in 
-          if (head_const (body_of_type typ)) = const then  
-            fn (pr_id idc) env (body_of_type typ)
-      | "CONSTANT" 
-      | "PARAMETER" ->
-	  let {const_type=typ} = Global.lookup_constant sp in
-	  if (head_const (body_of_type typ)) = const then
-            fn (pr_global (ConstRef sp)) env (body_of_type typ)
-      | "INDUCTIVE" -> 
-          let mib = Global.lookup_mind sp in 
-	  let arities =
-	    array_map_to_list 
-	      (fun mip ->
-		 (Name mip.mind_typename, None, mip.mind_nf_arity))
-	      mib.mind_packets in
-	  let env_ar = push_rels arities env in
-          (match kind_of_term const with 
-	     | IsMutInd ((sp',tyi),_) -> 
-		 if sp=sp' then (*Suffit pas, cf les inds de Ensemble.v*)
-		   print_constructors fn env_ar
-		     (mind_nth_type_packet mib tyi)
-	     | _ -> ())
-      | _ -> ()
-  in 
-  try 
-    Library.iter_all_segments false crible_rec 
-  with Not_found -> 
-    errorlabstrm "search"
-      [< pr_global ref; 'sPC; 'sTR "not declared" >]
-
-let search_by_head ref =
-  crible (fun pname ass_name constr -> 
-            let pc = prterm_env ass_name constr in
-            mSG[< pname; 'sTR":"; pc; 'fNL >]) ref
-
 let read_sec_context sec =
   let rec get_cxt in_cxt = function
     | ((sp,Lib.OpenedSection str) as hd)::rest ->
diff --git a/parsing/pretty.mli b/parsing/pretty.mli
index 0c792094b..94bdcea67 100644
--- a/parsing/pretty.mli
+++ b/parsing/pretty.mli
@@ -46,7 +46,5 @@ val print_coercions : unit -> std_ppcmds
 val print_path_between : identifier -> identifier -> std_ppcmds
 
 
-val search_by_head : global_reference -> unit
-val crible : (std_ppcmds -> env -> constr -> unit) -> global_reference -> unit
 val inspect : int -> std_ppcmds
 
diff --git a/parsing/search.ml b/parsing/search.ml
new file mode 100644
index 000000000..96d35cc46
--- /dev/null
+++ b/parsing/search.ml
@@ -0,0 +1,175 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Term
+open Declarations
+open Libobject
+open Declare
+open Coqast
+open Astterm
+open Pretty
+open Environ
+open Pattern
+open Printer
+
+(* The functions print_constructors and crible implement the behavior needed
+   for the Coq Search command.
+   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 fn env_ar mip = 
+  let _ =
+    array_map2 (fun id c -> fn (pr_id id) (* il faudrait qualifier... *)
+		    env_ar (body_of_type c))
+    mip.mind_consnames (mind_user_lc mip)
+  in ()
+
+let rec head_const c = match kind_of_term c with
+  | IsProd (_,_,d) -> head_const d
+  | IsLetIn (_,_,_,d) -> head_const d
+  | IsApp (f,_)   -> head_const f
+  | IsCast (d,_)   -> head_const d
+  | _            -> c
+
+let crible (fn : std_ppcmds -> env -> constr -> unit) ref =
+  let env = Global.env () in
+  let imported = Library.opened_modules() in
+  let const = constr_of_reference Evd.empty env ref in 
+  let crible_rec sp lobj =
+    match object_tag lobj with
+      | "VARIABLE" ->
+	  let ((idc,_,typ),_,_) = get_variable sp in 
+          if (head_const (body_of_type typ)) = const then  
+            fn (pr_id idc) env (body_of_type typ)
+      | "CONSTANT" 
+      | "PARAMETER" ->
+	  let {const_type=typ} = Global.lookup_constant sp in
+	  if (head_const (body_of_type typ)) = const then
+            fn (pr_global (ConstRef sp)) env (body_of_type typ)
+      | "INDUCTIVE" -> 
+          let mib = Global.lookup_mind sp in 
+	  let arities =
+	    array_map_to_list 
+	      (fun mip ->
+		 (Name mip.mind_typename, None, mip.mind_nf_arity))
+	      mib.mind_packets in
+	  let env_ar = push_rels arities env in
+          (match kind_of_term const with 
+	     | IsMutInd ((sp',tyi),_) -> 
+		 if sp=sp' then (*Suffit pas, cf les inds de Ensemble.v*)
+		   print_constructors fn env_ar
+		     (mind_nth_type_packet mib tyi)
+	     | _ -> ())
+      | _ -> ()
+  in 
+  try 
+    Library.iter_all_segments false crible_rec 
+  with Not_found -> 
+    errorlabstrm "search"
+      [< pr_global ref; 'sPC; 'sTR "not declared" >]
+
+let search_by_head ref =
+  crible (fun pname ass_name constr -> 
+            let pc = prterm_env ass_name constr in
+            mSG[< pname; 'sTR":"; pc; 'fNL >]) 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
+  | IsProd (_,_,c) -> head c
+  | _              -> c
+      
+let constr_to_section_path c = match kind_of_term c with
+  | IsConst (sp,_) -> sp
+  | _ -> raise No_section_path
+      
+let xor a b = (a or b) & (not (a & b))
+
+let plain_display s a c =
+  let pc = Printer.prterm_env a c in
+  mSG [< s; 'sTR":"; pc; 'fNL>]
+
+let filter_by_module module_list accept _ _ c =
+  try
+    let sp = constr_to_section_path c in
+    let sl = dirpath sp in
+    let rec filter_aux = function
+      | m :: tl -> (not (List.mem m sl)) && (filter_aux tl)
+      | [] -> true 
+    in
+    xor accept (filter_aux module_list)
+  with No_section_path -> 
+    false
+
+let gref_eq = IndRef (make_path ["Logic"] (id_of_string "eq") CCI, 0)
+
+let mk_rewrite_pattern1 pattern =
+  PApp (PRef gref_eq, [| PMeta None; pattern; PMeta None |])
+
+let mk_rewrite_pattern2 pattern =
+  PApp (PRef gref_eq, [| PMeta None; PMeta None; pattern |])
+
+let pattern_filter pat _ a c =
+  try 
+    try
+      Pattern.is_matching pat (head c) 
+    with _ -> 
+      Pattern.is_matching
+	pat (head (Typing.type_of (Global.env()) Evd.empty c))
+    with UserError _ -> 
+      false
+
+let filtered_search filter_function display_function ref =
+  crible 
+    (fun s a c -> if filter_function s a c then display_function s a c) 
+    ref
+
+let rec id_from_pattern = function
+  | PRef gr -> gr
+  | PVar id -> Nametab.sp_of_id CCI id
+  | PApp (p,_) -> id_from_pattern p
+  | _ -> error "the pattern is not simple enough"
+	
+let 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 search_rewrite extra_filter display_function pattern =
+  filtered_search
+    (fun s a c ->
+       ((pattern_filter (mk_rewrite_pattern1 pattern) s a c) ||
+        (pattern_filter (mk_rewrite_pattern2 pattern) s a c)) 
+       && extra_filter s a c)
+    display_function gref_eq
+
+let text_pattern_search extra_filter =
+  pattern_search extra_filter plain_display
+    
+let text_search_rewrite extra_filter =
+  search_rewrite extra_filter plain_display
+
+let filter_by_module_from_list = function
+  | [], _ -> (fun _ _ _ -> true)
+  | l, s -> filter_by_module l (s = "inside")
+
+let search_modules ref inout = 
+  filtered_search (filter_by_module_from_list inout) plain_display ref
+
+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
+
+
diff --git a/parsing/search.mli b/parsing/search.mli
new file mode 100644
index 000000000..42e277a5d
--- /dev/null
+++ b/parsing/search.mli
@@ -0,0 +1,17 @@
+
+(* $Id$ *)
+
+open Pp
+open Term
+open Environ
+open Pattern
+
+(*s Search facilities. *)
+
+val crible : (std_ppcmds -> env -> constr -> unit) -> global_reference -> unit
+
+val search_by_head : global_reference -> unit
+
+val search_modules : global_reference -> string list * string -> unit
+val search_rewrite : Pattern.constr_pattern  -> string list * string -> unit
+val search_pattern : Pattern.constr_pattern  -> string list * string -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8bf20ca69..1f0524aaf 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -888,11 +888,12 @@ let _ =
        | [VARG_QUALID qid] ->
 	   (fun () ->
 	      let ref =
-		try Nametab.locate qid
+		try 
+		  Nametab.locate qid
 		with Not_found ->
 		  Pretype_errors.error_global_not_found_loc loc qid
 	      in 
-	      search_by_head ref)
+	      Search.search_by_head ref)
        | _ -> bad_vernac_args "SEARCH")
 
 let _ =
@@ -901,6 +902,43 @@ let _ =
        | [VARG_NUMBER n] -> (fun () -> mSG(inspect n))
        | _ -> bad_vernac_args "INSPECT")
 
+let string_of_id_list =
+  List.map (function 
+	      | VARG_IDENTIFIER s -> string_of_id s
+	      | _ -> bad_vernac_args "string_of_id_list")
+
+let inside_outside = function
+  | (VARG_STRING s) :: l -> string_of_id_list l, s
+  | [] -> [], ""
+  | _ -> bad_vernac_args "inside/outside"
+
+let _ =
+  add "SearchModules"
+    (function
+       | (VARG_IDENTIFIER id) :: l ->
+           (fun () -> 
+	      let ref = Nametab.sp_of_id CCI id in
+              Search.search_modules ref (inside_outside l))
+       | _ -> bad_vernac_args "SearchModules")
+
+let _ = 
+  add "SearchRewrite"
+    (function
+       | (VARG_CONSTR c) :: l ->
+	   (fun () -> 
+	      let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
+	      Search.search_rewrite pat (inside_outside l))
+       | _ -> bad_vernac_args "SearchRewrite")
+
+let _ = 
+  add "SearchPattern"
+    (function
+       | (VARG_CONSTR c) :: l ->
+	   (fun () -> 
+	      let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
+	      Search.search_pattern  pat (inside_outside l))
+       | _ -> bad_vernac_args "SearchPattern")
+
 let _ =
   add "SETUNDO"
     (function