1 files changed, 0 insertions, 49 deletions
diff --git a/kernel/term.ml b/kernel/term.ml
index b09bd4aea..ad4bd2bda 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1177,52 +1177,3 @@ let (hcons1_constr, hcons1_types) = hcons_constr (hcons_names())
 (*******)
 (* Type of abstract machine values *)
 type values
-
-
-
-(* spiwack : internal representation printing *)
-let string_of_sorts =
-  function 
-  | Prop Pos -> "Prop Pos"
-  | Prop Null -> "Prop Null"
-  | Type u -> "Type "^string_of_universe u
-
-let string_of_cast_kind = 
-  function
-  |VMcast -> "VMcast"
-  | DEFAULTcast -> "DEFAULTcast"
-
-let rec string_of_constr = 
-  let string_of_term string_of_expr string_of_type = function
-  | Rel i -> "Rel "^string_of_int i
-  | Var id -> "Var "^string_of_identifier id
-  | Meta mv -> "Meta "^"mv?" (* need a function for printing metavariables *)
-  | Evar ev -> "Evar "^"ev?" (* ??     of 'constr pexistential *)
-  | Sort s -> "Sort "^string_of_sorts s
-  | Cast (e,ck,t) -> 
-         "Cast ("^string_of_expr e^", "^string_of_cast_kind ck^", "^
-                 string_of_type t^")" 
-  | Prod (n, t1, t2) -> 
-          "Prod ("^string_of_name n^", "^string_of_type t1^", "^
-                   string_of_type t2^")"  
-  | Lambda (n,t,e) ->
-          "Lambda ("^string_of_name n^", "^string_of_type t^", "^
-                    string_of_expr e^")"
-  | LetIn (n, e1, t, e2) -> 
-           "LetIn ("^string_of_name n^", "^string_of_expr e1^", "^
-           string_of_type t^", "^string_of_expr e2^")"
-  | App   (e, args) ->  "App ("^string_of_expr e^", [|"^
-          String.concat "; " (Array.to_list (Array.map string_of_expr args)) ^
-          "|])"
-  | Const c ->  "Const "^string_of_constant c
-  | Ind   ind ->  "Ind "^string_of_inductive ind
-  | Construct ctr -> "Construct "^string_of_constructor ctr
-  | Case(_,_,_,_)  -> "Case ..."    
-             (*    of case_info * 'constr * 'constr * 'constr array   *)
-  | Fix _  -> "Fix ..."  (*    of ('constr, 'types) pfixpoint *)
-  | CoFix _ -> "CoFix ..."  (*     of ('constr, 'types) pcofixpoint *)
-in 
-fun x -> string_of_term string_of_constr string_of_constr x
-
-
-(* /spiwack *)