1 files changed, 3 insertions, 32 deletions
diff --git a/kernel/term.ml b/kernel/term.ml
index 4416770fe4..62c161be4c 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -8,7 +8,7 @@
 
 open Util
 open Pp
-open Errors
+open CErrors
 open Names
 open Vars
 
@@ -328,38 +328,9 @@ let destCoFix c = match kind_of_term c with
 let isCoFix c =  match kind_of_term c with CoFix _ -> true | _ -> false
 
 (******************************************************************)
-(* Cast management                                                *)
-(******************************************************************)
-
-let rec strip_outer_cast c = match kind_of_term c with
-  | Cast (c,_,_) -> strip_outer_cast c
-  | _ -> c
-
-(* Fonction spéciale qui laisse les cast clés sous les Fix ou les Case *)
-
-let under_outer_cast f c =  match kind_of_term c with
-  | Cast (b,k,t) -> mkCast (f b, k, f t)
-  | _ -> f c
-
-let rec under_casts f c = match kind_of_term c with
-  | Cast (c,k,t) -> mkCast (under_casts f c, k, t)
-  | _            -> f c
-
-(******************************************************************)
 (* Flattening and unflattening of embedded applications and casts *)
 (******************************************************************)
 
-(* flattens application lists throwing casts in-between *)
-let collapse_appl c = match kind_of_term c with
-  | App (f,cl) ->
-      let rec collapse_rec f cl2 =
-        match kind_of_term (strip_outer_cast f) with
-        | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
-        | _ -> mkApp (f,cl2)
-      in
-      collapse_rec f cl
-  | _ -> c
-
 let decompose_app c =
   match kind_of_term c with
     | App (f,cl) -> (f, Array.to_list cl)
@@ -465,7 +436,7 @@ let rec to_lambda n prod =
     match kind_of_term prod with
       | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd)
       | Cast (c,_,_) -> to_lambda n c
-      | _   -> errorlabstrm "to_lambda" (mt ())
+      | _   -> user_err ~hdr:"to_lambda" (mt ())
 
 let rec to_prod n lam =
   if Int.equal n 0 then
@@ -474,7 +445,7 @@ let rec to_prod n lam =
     match kind_of_term lam with
       | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd)
       | Cast (c,_,_) -> to_prod n c
-      | _   -> errorlabstrm "to_prod" (mt ())
+      | _   -> user_err ~hdr:"to_prod" (mt ())
 
 let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
 let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)