From dc58e20b610718080da9a4bdb4db4ac7780be8f9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Apr 2008 13:07:54 +0000 Subject: [PATCH] removed useless file --- helm/software/components/ng_kernel/.depend | 2 -- .../software/components/ng_kernel/.depend.opt | 2 -- helm/software/components/ng_kernel/Makefile | 1 - .../components/ng_kernel/oCicTypeChecker.ml | 9 ------ .../components/ng_kernel/oCicTypeChecker.mli | 30 ------------------- 5 files changed, 44 deletions(-) delete mode 100644 helm/software/components/ng_kernel/oCicTypeChecker.ml delete mode 100644 helm/software/components/ng_kernel/oCicTypeChecker.mli 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 - -- 2.39.2