From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 5 May 2008 13:31:59 +0000 (+0000)
Subject: removed dead code
X-Git-Tag: make_still_working~5255
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f5e4a6c59a95c7f78e36924bce433abf8d59bf87;p=helm.git

removed dead code
---

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 0d3a265bb..118bc6911 100644
--- 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 a45d8422f..8c047c4c1 100644
--- 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 ->