SearchPattern et SearchRewrite

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

1 files changed, 0 insertions, 63 deletions

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 ->