+
+(*
+let convert_context uri =
+ let name_of = function Cic.Name s -> s | _ -> "_" in
+ List.fold_right
+ (function
+ | (Some (s, Cic.Decl t) as e) -> fun (nc,auxc,oc) ->
+ let t, _ = aux true oc auxc 0 uri t in
+ (name_of s, NCic.Decl t) :: nc,
+ Ce (lazy ((name_of s, NCic.Decl t),[])) :: auxc, e :: oc
+ | (Some (Cic.Name s, Cic.Def (t,ty)) as e) -> fun (nc,auxc,oc) ->
+ let t, _ = aux true oc auxc 0 uri t in
+ 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 -> nc, , e :: oc
+;;
+
+let convert_term uri ctx t =
+ aux false [] [] 0 uri t
+;;
+*)