| Cic.Variable (_, Some body, _, _, _), _ -> true
| _ -> false
-let string_of_uriref s =
- UriManager.uri_of_string (UriManager.string_of_uriref s)
-
let compute_term pos term =
let rec aux (pos: position) set = function
| Cic.Var (uri, subst) when var_has_body uri ->
(fun set (_, term) -> aux (next_pos pos) set term)
set subst
| Cic.MutInd (uri, typeno, subst) ->
- let uri = string_of_uriref (uri, [typeno]) in
+ let uri = UriManager.uri_of_uriref uri typeno None in
let set = S.add (`Obj (uri, pos)) set in
List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
set subst
| Cic.MutConstruct (uri, typeno, consno, subst) ->
- let uri = string_of_uriref (uri, [typeno; consno]) in
+ let uri = UriManager.uri_of_uriref uri typeno (Some consno) in
let set = S.add (`Obj (uri, pos)) set in
List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
set subst
let compute_type pos uri typeno (name, _, ty, constructors) =
let consno = ref 0 in
let type_metadata =
- (string_of_uriref (uri, [typeno]), name, (compute_term pos ty))
+ (UriManager.uri_of_uriref uri typeno None, name, (compute_term pos ty))
in
let constructors_metadata =
List.map
(fun (name, term) ->
incr consno;
- let uri = string_of_uriref (uri, [typeno; !consno]) in
+ let uri = UriManager.uri_of_uriref uri typeno (Some !consno) in
(uri, name, (compute_term pos term)))
constructors
in