removed useless file

diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend
index 11b70ea0fdacc13ca8de7a1ca9a5849735768f1c..faeadf95eb3aeef9e3acd412506c5392c012095f 100644 (file)
--- 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 4a637b8049aabd7916d009b1f3c42f3023289fef..ed86d2687c70cf148873c13a264f599de2fb7d6f 100644 (file)
--- 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 56915b13e6d16e813f56e969e794b3cb2e9dccb0..1870f381c34227d76eba28280aa7b6f8849f15b2 100644 (file)
--- 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 (file)
index 396144a..0000000
--- 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 (file)
index 1655343..0000000
--- 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
-