module U = NUri
module C = NCic
-module R = NReference
module E = NCicEnvironment
module T = NCicTypeChecker
P.sprintf "Type[%s]" (U.string_of_uri u)
| C.Sort (C.Type [`CProp, u]) ->
P.sprintf "CProp[%s]" (U.string_of_uri u)
- | C.Const (R.Ref (u, r)) ->
- let ss = K.segments_of_uri u in
- let _, _, _, _, obj = E.get_checked_obj G.status u in
- let ss, _ = K.name_of_reference ss (obj, r) in
- X.rev_map_concat X.id "." "type" ss
+ | C.Const c ->
+ let s, _ = K.resolve_reference c in
+ s
| _ -> ""
let read l s r =
try
let i = H.find st.g s in
H.replace st.g s (succ i);
- P.sprintf "%s.%u" s i
+ P.sprintf "%s_%u" s i
with Not_found ->
H.add st.g s 0;
s
let proc_named_term s st t =
try
let tt = proc_term st t in
- if !G.test then begin
+ if !G.check then begin
let _ = K.typeof st.c tt in
ok s
end;
tt
with
+ | E.ObjectNotFound s
| T.TypeCheckerFailure s
| T.AssertFailure s -> malformed (Lazy.force s)
(* interface functions ******************************************************)
let process_top_term s t = proc_named_term s (init ()) t
-