let module C = Cic in
match hyp with
None -> assert false
+ | Some (_, C.Def (_, Some _)) -> assert false
| Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
- | Some (n_to_clear_body, C.Def term) as hyp_to_clear_body ->
+ | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body ->
let curi,metasenv,pbo,pty = proof in
- let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,_,_ = CicUtil.lookup_meta goal metasenv in
let string_of_name =
function
C.Name n -> n
cleared_entry::context
| None -> None::context
| Some (n,C.Decl t)
- | Some (n,C.Def t) ->
+ | Some (n,C.Def (t,None)) ->
let _ =
try
CicTypeChecker.type_of_aux' metasenv context t
)
in
entry::context
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) canonical_context []
in
let _ =
| Some (n_to_clear, _) ->
let curi,metasenv,pbo,pty = proof in
let metano,context,ty =
- List.find (function (m,_,_) -> m=goal) metasenv
+ CicUtil.lookup_meta goal metasenv
in
let string_of_name =
function
match entry with
t when t == hyp_to_clear -> None::context
| None -> None::context
+ | Some (_,Cic.Def (_,Some _)) -> assert false
| Some (n,C.Decl t)
- | Some (n,C.Def t) ->
+ | Some (n,C.Def (t,None)) ->
let _ =
try
CicTypeChecker.type_of_aux' metasenv context t