(* ginve the old [goal], the side that has not changed [posu] and the
* expansion builds a new goal *)
(* ginve the old [goal], the side that has not changed [posu] and the
* expansion builds a new goal *)
let goalproof,_,_,_,_,_ = open_goal goal in
let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal posu expansion in
let pos, equality = eq_found in
let goalproof,_,_,_,_,_ = open_goal goal in
let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal posu expansion in
let pos, equality = eq_found in
- let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
bo, (newgoalproofstep::goalproof)
in
let newmetasenv = (* Inference.filter subst *) menv in
bo, (newgoalproofstep::goalproof)
in
let newmetasenv = (* Inference.filter subst *) menv in
match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
in
let expansions, _ = betaexpand_term menv context ugraph table 0 big in
match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
in
let expansions, _ = betaexpand_term menv context ugraph table 0 big in