let module C = Cic in
match hyp_to_clear with
None -> assert false
| Some (n_to_clear, _) ->
let curi,metasenv,pbo,pty = proof in
let metano,context,ty =
let module C = Cic in
match hyp_to_clear with
None -> assert false
| Some (n_to_clear, _) ->
let curi,metasenv,pbo,pty = proof in
let metano,context,ty =