let proof, goalno = status in
let _, metasenv,_,_ = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let eq_uri = eq_of_goal type_of_goal in
let env = (metasenv, context, CicUniv.empty_ugraph) in
let eq_indexes, equalities, maxm, cache =
let proof, goalno = status in
let _, metasenv,_,_ = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let eq_uri = eq_of_goal type_of_goal in
let env = (metasenv, context, CicUniv.empty_ugraph) in
let eq_indexes, equalities, maxm, cache =