From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 1 Oct 2008 14:24:04 +0000 (+0000)
Subject: commented out unfinished code
X-Git-Tag: make_still_working~4715
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=208c4a16cab77ee59df58f0720d8ec9d29189523;p=helm.git

commented out unfinished code
---

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 0854b624f..88bdf4f00 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -845,6 +845,7 @@ let convert_obj uri obj =
   fixpoints @ [obj]
 ;;
 
+(*
 let convert_context uri =
   let name_of = function Cic.Name s -> s | _ -> "_" in
   List.fold_right
@@ -858,9 +859,10 @@ let convert_context uri =
        let t, _ = aux true oc auxc 0 uri ty in
        (name_of s, NCic.Def (t,ty)) :: nc, 
        Ce (lazy ((name_of s, NCic.Def (t,ty)),[])) :: auxc,  e :: oc
-    | None -> ...
+    | None -> nc, , e :: oc
 ;;
 
 let convert_term uri ctx t = 
    aux false [] [] 0 uri t
 ;;
+*)
diff --git a/helm/software/components/ng_kernel/oCic2NCic.mli b/helm/software/components/ng_kernel/oCic2NCic.mli
index 02ee706ef..b1351ae28 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.mli
+++ b/helm/software/components/ng_kernel/oCic2NCic.mli
@@ -16,4 +16,4 @@ val nuri_of_ouri: UriManager.uri -> NUri.uri
 val reference_of_ouri: UriManager.uri -> NReference.spec -> NReference.reference
 
 val convert_obj: UriManager.uri -> Cic.obj -> NCic.obj list
-val convert_term: UriManager.uri -> Cic.term -> NCic.term * NCic.obj list
+(* val convert_term: UriManager.uri -> Cic.term -> NCic.term * NCic.obj list *)