using the new by foo we proved semantics

[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml

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
 ;;
+*)