commented out unfinished code

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 0854b624f157aa486fd8aae0f67f2eadd7bb9389..88bdf4f00e620fc7194d7cfd2083a90106abefd3 100644 (file)
--- 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 02ee706efa1fa597da0df7b5b58a3b3c024d129c..b1351ae287272c199d111ca0d9a963d894a5bd7d 100644 (file)
--- 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 *)