removed dead code

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 0d3a265bb0efb7dda01e526630cd3c4b4f3f44cc..118bc6911ad9e1149a66887b871074fd85a5ac07 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -13,28 +13,6 @@
 
 (* TODO unify exceptions *)
 
-exception WrongUriToInductiveDefinition;;
-exception Impossible of int;;
-exception ReferenceToConstant;;
-exception ReferenceToVariable;;
-exception ReferenceToCurrentProof;;
-exception ReferenceToInductiveDefinition;;
-
-let debug = false
-let profile = false
-let debug_print s = if debug then prerr_endline (Lazy.force s)
-
-let fdebug = ref 1;;
-let debug t env s =
- let rec debug_aux t i =
-  let module C = Cic in
-  let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
- in
-  if !fdebug = 0 then
-   debug_print (lazy (s ^ "\n" ^ List.fold_right debug_aux (t::env) ""))
-;;
-
 module type Strategy =
  sig
   type stack_term

diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli
index a45d8422f8ead2bced870fb2a61f331803806233..8c047c4c183d293a791d63f7e82c4b805623b08b 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.mli
+++ b/helm/software/components/ng_kernel/nCicReduction.mli
@@ -23,12 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception WrongUriToInductiveDefinition
-exception ReferenceToConstant
-exception ReferenceToVariable
-exception ReferenceToCurrentProof
-exception ReferenceToInductiveDefinition
-
 val whd : 
   ?delta:int -> ?subst:NCic.substitution -> 
   NCic.context -> NCic.term ->