(match spec with
| NReference.Def _ -> NReference.Def height
| NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
- | NReference.CoFix _ -> NReference.CoFix height
+ | NReference.CoFix i -> NReference.CoFix i
| NReference.Ind _ | NReference.Con _
| NReference.Decl as s -> s))
| t -> NCicUtils.map status (fun _ () -> ()) () fix t
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
) status boxml in
let _,_,_,_,nobj = obj in
let status = match nobj with
- NCic.Inductive (is_ind,leftno,[it],_) ->
- let _,ind_name,ty,cl = it in
- List.fold_left
+ NCic.Inductive (is_ind,leftno,itl,_) ->
+ List.fold_left (fun status it ->
+ (let _,ind_name,ty,cl = it in
+ List.fold_left
(fun status outsort ->
let status = status#set_ng_mode `ProofMode in
try
let status = status#set_ng_mode `CommandMode in status)
status
(NCic.Prop::
- List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ()))
+ List.map (fun s -> NCic.Type s)
+ (NCicEnvironment.get_universes ())))) status itl
| _ -> status
in
let status = match nobj with
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