- let obj =
-prerr_endline "CSC: here we should fix the height!!!";
- (uri,height,[],[],
- NCicUntrusted.map_obj_kind
- (NCicUntrusted.apply_subst subst [])
- obj) in
- NCicTypeChecker.typecheck_obj obj;
- NCicLibrary.add_obj uri obj;
- let objs = NCicElim.mk_elims obj in
- let uris =
- uri::
- List.map
- (fun (uri,_,_,_,_) as obj ->
- NCicTypeChecker.typecheck_obj obj;
- NCicLibrary.add_obj uri obj;
- uri
- ) objs
- in
- {status with
+ let obj_kind =
+ NCicUntrusted.map_obj_kind
+ (NCicUntrusted.apply_subst subst []) obj_kind in
+ let height = NCicUntrusted.height_of_obj_kind uri obj_kind in
+ let obj = uri,height,[],[],obj_kind in
+ NCicTypeChecker.typecheck_obj obj;
+ NCicLibrary.add_obj uri obj;
+ let objs = NCicElim.mk_elims obj in
+ let uris =
+ uri::
+ List.map
+ (fun (uri,_,_,_,_) as obj ->
+ NCicTypeChecker.typecheck_obj obj;
+ NCicLibrary.add_obj uri obj;
+ uri
+ ) objs
+ in
+ {status with