* Major code cleanup.

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index f2cd6265e5887a6f02edad77e8032b2194175725..28089b4cc059ea9bfdbe929adeb755cef2198721 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -63,33 +63,7 @@ let debug t env =
  let rec debug_aux t i =
   let module C = Cic in
   let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG", None,
-    C.Prod (C.Name "-15", C.Const (U.uri_of_string "cic:/dummy-15",0),
-    C.Prod (C.Name "-14", C.Const (U.uri_of_string "cic:/dummy-14",0),
-    C.Prod (C.Name "-13", C.Const (U.uri_of_string "cic:/dummy-13",0),
-    C.Prod (C.Name "-12", C.Const (U.uri_of_string "cic:/dummy-12",0),
-    C.Prod (C.Name "-11", C.Const (U.uri_of_string "cic:/dummy-11",0),
-    C.Prod (C.Name "-10", C.Const (U.uri_of_string "cic:/dummy-10",0),
-    C.Prod (C.Name "-9", C.Const (U.uri_of_string "cic:/dummy-9",0),
-    C.Prod (C.Name "-8", C.Const (U.uri_of_string "cic:/dummy-8",0),
-    C.Prod (C.Name "-7", C.Const (U.uri_of_string "cic:/dummy-7",0),
-    C.Prod (C.Name "-6", C.Const (U.uri_of_string "cic:/dummy-6",0),
-     C.Prod (C.Name "-5", C.Const (U.uri_of_string "cic:/dummy-5",0),
-      C.Prod (C.Name "-4", C.Const (U.uri_of_string "cic:/dummy-4",0),
-       C.Prod (C.Name "-3", C.Const (U.uri_of_string "cic:/dummy-3",0),
-        C.Prod (C.Name "-2", C.Const (U.uri_of_string "cic:/dummy-2",0),
-         C.Prod (C.Name "-1", C.Const (U.uri_of_string "cic:/dummy-1",0),
-          t
-         )
-        )
-       )
-      )
-     )
-    )
-    )
-    )
-    )))))))
-    )) ^ "\n" ^ i
+   CicPp.ppobj (C.Variable ("DEBUG", None, t)) ^ "\n" ^ i
  in
   if !fdebug = 0 then
    raise (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::env) ""))