- let obj =
-prerr_endline "CSC: here we should fix the height!!!";
- uri,height,[],[],NTacStatus.apply_subst_obj subst obj
- in
- NCicLibrary.add_obj uri obj;
- {status with
- GrafiteTypes.ng_status =
- GrafiteTypes.CommandMode lexicon_status },[]
+ let obj_kind =
+ NCicUntrusted.map_obj_kind
+ (NCicUntrusted.apply_subst subst []) obj_kind in
+ let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in
+ let obj = uri,height,[],[],obj_kind in
+ NCicTypeChecker.typecheck_obj obj;
+ let timestamp = NCicLibrary.add_obj uri obj in
+ let objs = NCicElim.mk_elims obj in
+ let timestamp,uris_rev =
+ List.fold_left
+ (fun (timestamp,uris_rev) (uri,_,_,_,_) as obj ->
+ NCicTypeChecker.typecheck_obj obj;
+ let timestamp = NCicLibrary.add_obj uri obj in
+ timestamp,uri::uris_rev
+ ) (timestamp,[]) objs in
+ let uris = uri::List.rev uris_rev in
+ GrafiteTypes.set_library_db timestamp
+ {status with
+ GrafiteTypes.ng_status =
+ GrafiteTypes.CommandMode estatus },`New uris