From f5e4a6c59a95c7f78e36924bce433abf8d59bf87 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 May 2008 13:31:59 +0000 Subject: [PATCH] removed dead code --- .../components/ng_kernel/nCicReduction.ml | 22 ------------------- .../components/ng_kernel/nCicReduction.mli | 6 ----- 2 files changed, 28 deletions(-) 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 -> -- 2.39.2