- [] ->
- (* CSC: cut&paste code from NQed *)
- let obj =
-prerr_endline "CSC: here we should fix the height!!!";
- uri,height,[],[],NTacStatus.apply_subst_obj nsubst nobj
- in
- NCicLibrary.add_obj uri obj;
- {status with
- GrafiteTypes.ng_status=GrafiteTypes.CommandMode lexicon_status },
- `New [uri]
- | _ ->
- let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
- { status with
- GrafiteTypes.ng_status =
- GrafiteTypes.ProofMode
- { NTacStatus.gstatus = ninitial_stack;
- istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}}
- },`New [])
+ [] ->
+ eval_command.ec_go ~disambiguate_command opts status
+ ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ | _ -> status,`New [])