try
let nstatus =
eval_ncommand ~include_paths opts status
- ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
+ ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml,true))
in
if nstatus#ng_mode <> `CommandMode then
begin
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))
- | GrafiteAst.NObj (loc,obj) ->
+ | GrafiteAst.NObj (loc,obj,index) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
else
let status = status#set_ng_mode `ProofMode in
(match nmenv with
[] ->
- eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,true))
+ eval_ncommand ~include_paths opts status
+ ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,index))
| _ -> status)
| GrafiteAst.NDiscriminator (loc, indty) ->
if status#ng_mode <> `CommandMode then