- NCicLibrary.add_obj uri obj;
- {status with
- GrafiteTypes.ng_status =
- GrafiteTypes.CommandMode lexicon_status },`New [uri]
+ let obj_kind =
+ match obj_kind with
+ | NCic.Fixpoint _ ->
+ NCicUntrusted.map_obj_kind (fix ()) obj_kind
+ | _ -> 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