let status = subst_metasenv_and_fix_names status in
let status = status#set_ng_mode `ProofMode in
eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
let status = subst_metasenv_and_fix_names status in
let status = status#set_ng_mode `ProofMode in
eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))