let metasenv = toposort metasenv in
let bo = close_in_context bo metasenv in
let pos =
match p with
| NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv)
let metasenv = toposort metasenv in
let bo = close_in_context bo metasenv in
let pos =
match p with
| NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv)