1 files changed, 0 insertions, 88 deletions
diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml
index e63baecf..6e4782be 100644
--- a/contrib/interface/translate.ml
+++ b/contrib/interface/translate.ml
@@ -1,13 +1,11 @@
 open Names;;
 open Sign;;
 open Util;;
-open Ast;;
 open Term;;
 open Pp;;
 open Libobject;;
 open Library;;
 open Vernacinterp;;
-open Termast;;
 open Tacmach;;
 open Pfedit;;
 open Parsing;;
@@ -15,97 +13,11 @@ open Evd;;
 open Evarutil;;
 
 open Xlate;;
-open Ctast;;
 open Vtp;;
 open Ascent;;
 open Environ;;
 open Proof_type;;
 
-(* dead code: let rel_reference gt k oper = 
- if is_existential_oper oper then ope("XTRA", [str "ISEVAR"])
- else begin
-  let id = id_of_global oper in
-  let oper', _ = global_operator (Nametab.sp_of_id k id) id in
-  if oper = oper' then nvar (string_of_id id)
-  else failwith "xlate"
-end;;
-*)
-
-(* dead code: 
-let relativize relfun =
- let rec relrec =
-  function
-     | Nvar (_, id) -> nvar id
-     | Slam (l, na, ast) -> Slam (l, na, relrec ast)
-     | Node (loc, nna, l) as ast -> begin
-       try relfun ast
-       with
-       | Failure _ -> Node (loc, nna, List.map relrec l)
-     end
-     | a -> a in
- relrec;;
-*)
-
-(* dead code:
-let dbize_sp =
- function
-    | Path (loc, sl, s) -> begin
-      try section_path sl s
-      with
-      | Invalid_argument _ | Failure _ ->
-      anomaly_loc
-       (loc, "Translate.dbize_sp (taken from Astterm)",
-       [< str "malformed section-path" >])
-    end
-    | ast ->
-     anomaly_loc
-      (Ast.loc ast, "Translate.dbize_sp (taken from Astterm)",
-      [< str "not a section-path" >]);;
-*)
-
-(* dead code:
-let relativize_cci gt = relativize (function
-    | Node (_, "CONST", (p :: _)) as gt ->
-     rel_reference gt CCI (Const (dbize_sp p))
-    | Node (_, "MUTIND", (p :: ((Num (_, tyi)) :: _))) as gt ->
-     rel_reference gt CCI (MutInd (dbize_sp p, tyi))
-    | Node (_, "MUTCONSTRUCT", (p :: ((Num (_, tyi)) :: ((Num (_, i)) :: _)))) as gt ->
-     rel_reference gt CCI (MutConstruct (
-      (dbize_sp p, tyi), i))
-    | _ -> failwith "caught") gt;;
-*)
-
-let coercion_description_holder = ref (function _ -> None : t -> int option);;
-
-let coercion_description t = !coercion_description_holder t;;
-
-let set_coercion_description f =
- coercion_description_holder:=f; ();;
-
-let rec nth_tl l n = if n = 0 then l
- else (match l with
- | a :: b -> nth_tl b (n - 1)
- | [] -> failwith "list too short for nth_tl");;
-
-let rec discard_coercions =
- function
-    | Slam (l, na, ast) -> Slam (l, na, discard_coercions ast)
-    | Node (l, ("APPLIST" as nna), (f :: args as all_sons)) ->
-     (match coercion_description f with
-     | Some n ->
-      let new_args =
-       try nth_tl args n
-       with
-       | Failure "list too short for nth_tl" -> [] in
-      (match new_args with
-       | a :: (b :: c) -> Node (l, nna, List.map discard_coercions new_args)
-       | a :: [] -> discard_coercions a
-       | [] -> Node (l, nna, List.map discard_coercions all_sons))
-     | None -> Node (l, nna, List.map discard_coercions all_sons))
-    | Node (l, nna, all_sons) ->
-     Node (l, nna, List.map discard_coercions all_sons)
-    | it -> it;;
-
 (*translates a formula into a centaur-tree --> FORMULA *)
 let translate_constr at_top env c =
   xlate_formula (Constrextern.extern_constr at_top env c);;