1 files changed, 0 insertions, 87 deletions
diff --git a/contrib/xml/cooking.ml b/contrib/xml/cooking.ml
deleted file mode 100644
index 10c8d80ef..000000000
--- a/contrib/xml/cooking.ml
+++ /dev/null
@@ -1,87 +0,0 @@
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     A tactic to print Coq objects in XML                   *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 02/12/1999                                 *)
-(*                                                                            *)
-(* This module compute the list of variables occurring in a term from the     *)
-(* term and the list of variables possibly occuring in it                     *)
-(*                                                                            *)
-(******************************************************************************)
-
-let get_depth_of_var vl v =
- let rec aux n =
-  function
-     [] -> None
-   | (he::tl) -> if List.mem v he then Some n else aux (n + 1) tl
- in
-  aux 0 vl
-;;
-
-exception CookingInternalError;;
-
-let string_of_vars_list =
- let add_prefix n s = string_of_int n ^ ": " ^ s in
- let rec aux =
-  function
-     [n,v] -> (n,v)
-   | (n,v)::tl ->
-      let (k,s) = aux tl in
-       if k = n then (k, v ^ " " ^ s) else (n, v ^ " " ^ add_prefix k s)
-   | [] -> raise CookingInternalError
- in
-  function
-     [] -> ""
-   | vl -> let (k,s) = aux vl in add_prefix k s
-;;
-
-(*CSC commento sbagliato ed obsoleto *)
-(* If t is \v1. ... \vn.t' where v1, ..., vn are in the variable list vl then *)
-(* get_params_from_type vl t returns [v1; ...; vn]                            *)
-let get_params_from_type vl t =
- let rec rget t l =
-  let module T = Term in
-  let module N = Names in
-   match T.kind_of_term t with
-      T.IsProd (N.Name id, _, target) ->
-       let id' = N.string_of_id id in
-        (match get_depth_of_var vl id' with
-            None   -> l
-          | Some n -> rget target ((n,id')::l)
-        )
-    | T.IsCast (term, _) -> rget term l
-    | _ -> l
- in
-  let pl = List.rev (rget t []) in
-   string_of_vars_list pl
-;;
-
-(* add_cooking_information csp vl                               *)
-(*  when  csp is the section path of the most cooked object co  *)
-(*  and   vl  is the list of variables possibly occuring in co  *)
-(* returns the list of variables actually occurring in co       *)
-let add_cooking_information sp vl =
- let module D = Declarations in
- let module G = Global in
- let module N = Names in
- let module T = Term in
- let module X = Xml in
-  try
-   let {D.const_body=val0 ; D.const_type = typ} = G.lookup_constant sp in
-   let typ = T.body_of_type typ in
-    get_params_from_type vl typ
-  with
-   Not_found ->
-    try
-     let {D.mind_packets=packs ; D.mind_nparams=nparams} =
-      G.lookup_mind sp
-     in
-      let {D.mind_nf_arity=arity} = packs.(0) in
-      let arity = T.body_of_type arity in
-       get_params_from_type vl arity
-    with
-     Not_found -> Util.anomaly "Cooking of an uncoockable term required"
-;;