Patch to add a debugging string to HExtlib.split_nth reverted

[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..2738b1c901835183078c7a24b0f3470475f13f02 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -458,11 +458,11 @@ prerr_endline ("CACHE SAME NAME: " ^ NReference.string_of_reference ref ^ " <==>
  with Found ref -> Some ref
 ;;
 
+let cache1 = UriManager.UriHashtbl.create 313;;
 let rec get_height =
- let cache = UriManager.UriHashtbl.create 313 in
    function u ->
      try
-       UriManager.UriHashtbl.find cache u
+       UriManager.UriHashtbl.find cache1 u
      with
       Not_found ->
         let h = ref 0 in
@@ -476,7 +476,7 @@ let rec get_height =
                1 + !h
            | _ -> 0
          in
-           UriManager.UriHashtbl.add cache u res;
+           UriManager.UriHashtbl.add cache1 u res;
            res
 and height_of_term ?(h=ref 0) t =
  let rec aux =
@@ -845,6 +845,12 @@ let convert_obj uri obj =
   fixpoints @ [obj]
 ;;
 
+let clear () =
+  Hashtbl.clear cache;
+  UriManager.UriHashtbl.clear cache1
+;;
+
+(*
 let convert_context uri =
   let name_of = function Cic.Name s -> s | _ -> "_" in
   List.fold_right
@@ -858,9 +864,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
 ;;
+*)