From 675d7c4310e10d68e876331a95c46b726494ed91 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 2 Sep 2016 10:09:04 +0200
Subject: Remove useless debug code.

---
 kernel/csymtable.ml | 14 +++-----------
 1 file changed, 3 insertions(+), 11 deletions(-)

(limited to 'kernel')

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index acd73d97d7..e195618b6b 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -219,17 +219,9 @@ and eval_to_patch env (buff,pl,fv) =
   eval_tcode tc vm_env
 
 and val_of_constr env c =
-  let (_,fun_code,_ as ccfv) =
-    try match compile true env c with
-	| Some v -> v
-	| None -> assert false
-    with reraise ->
-      let reraise = CErrors.push reraise in
-      let () = print_string "can not compile \n" in
-      let () = Format.print_flush () in
-      iraise reraise
-  in
-  eval_to_patch env (to_memory ccfv)
+  match compile true env c with
+  | Some v -> eval_to_patch env (to_memory v)
+  | None -> assert false
 
 let set_transparent_const kn = () (* !?! *)
 let set_opaque_const kn = () (* !?! *)
-- 
cgit v1.2.3