From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 11 Apr 2008 13:07:54 +0000 (+0000)
Subject: removed useless file
X-Git-Tag: make_still_working~5359
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dc58e20b610718080da9a4bdb4db4ac7780be8f9;p=helm.git

removed useless file
---

diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend
index 11b70ea0f..faeadf95e 100644
--- a/helm/software/components/ng_kernel/.depend
+++ b/helm/software/components/ng_kernel/.depend
@@ -35,7 +35,5 @@ nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \
 nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \
     nCicSubstitution.cmx nCicReduction.cmx nCicPp.cmx nCicEnvironment.cmx \
     nCic.cmx nCicTypeChecker.cmi 
-oCicTypeChecker.cmo: oCic2NCic.cmi nCicTypeChecker.cmi oCicTypeChecker.cmi 
-oCicTypeChecker.cmx: oCic2NCic.cmx nCicTypeChecker.cmx oCicTypeChecker.cmi 
 nCic2OCic.cmo: nUri.cmi nReference.cmi nCic.cmo nCic2OCic.cmi 
 nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi 
diff --git a/helm/software/components/ng_kernel/.depend.opt b/helm/software/components/ng_kernel/.depend.opt
index 4a637b804..ed86d2687 100644
--- a/helm/software/components/ng_kernel/.depend.opt
+++ b/helm/software/components/ng_kernel/.depend.opt
@@ -35,7 +35,5 @@ nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \
 nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \
     nCicSubstitution.cmx nCicReduction.cmx nCicPp.cmx nCicEnvironment.cmx \
     nCic.cmx nCicTypeChecker.cmi 
-oCicTypeChecker.cmo: oCic2NCic.cmi nCicTypeChecker.cmi oCicTypeChecker.cmi 
-oCicTypeChecker.cmx: oCic2NCic.cmx nCicTypeChecker.cmx oCicTypeChecker.cmi 
 nCic2OCic.cmo: nUri.cmi nReference.cmi nCic.cmx nCic2OCic.cmi 
 nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi 
diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile
index 56915b13e..1870f381c 100644
--- a/helm/software/components/ng_kernel/Makefile
+++ b/helm/software/components/ng_kernel/Makefile
@@ -11,7 +11,6 @@ INTERFACE_FILES = \
 	nCicPp.mli \
 	nCicReduction.mli \
 	nCicTypeChecker.mli \
-	oCicTypeChecker.mli \
 	nCic2OCic.mli
 
 IMPLEMENTATION_FILES = \
diff --git a/helm/software/components/ng_kernel/oCicTypeChecker.ml b/helm/software/components/ng_kernel/oCicTypeChecker.ml
deleted file mode 100644
index 396144a5d..000000000
--- a/helm/software/components/ng_kernel/oCicTypeChecker.ml
+++ /dev/null
@@ -1,9 +0,0 @@
-
-let typecheck_obj uri obj =
-  try 
-    NCicTypeChecker.typecheck_obj (HExtlib.list_last (OCic2NCic.convert_obj uri
-    obj)); true
-  with 
-    | NCicTypeChecker.TypeCheckerFailure _
-    | NCicTypeChecker.AssertFailure _ -> false
-
diff --git a/helm/software/components/ng_kernel/oCicTypeChecker.mli b/helm/software/components/ng_kernel/oCicTypeChecker.mli
deleted file mode 100644
index 165534310..000000000
--- a/helm/software/components/ng_kernel/oCicTypeChecker.mli
+++ /dev/null
@@ -1,30 +0,0 @@
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* typechecks the OLD object using the NEW type checker,
- * if illtyped returns false (no exceptions raised)
- *)
-val typecheck_obj : UriManager.uri -> Cic.obj -> bool
-