open ProofEngineTypes
-let clearbody ~status:(proof, goal) ~hyp =
+let clearbody ~hyp ~status:(proof, goal) =
let module C = Cic in
match hyp with
None -> assert false
| Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
| Some (n_to_clear_body, C.Def term) as hyp_to_clear_body ->
- let curi,metasenv,pbo,pty =
- match proof with
- None -> assert false
- | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
- let metano,_,_ =
- match goal with
- None -> assert false
- | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in
let string_of_name =
function
C.Name n -> n
| t -> t
) metasenv
in
- (Some (curi,metasenv',pbo,pty), goal)
+ (curi,metasenv',pbo,pty), [goal]
-let clear ~status:(proof, goal) ~hyp:hyp_to_clear =
+let clear ~hyp:hyp_to_clear ~status:(proof, goal) =
let module C = Cic in
match hyp_to_clear with
None -> assert false
| Some (n_to_clear, _) ->
- let curi,metasenv,pbo,pty =
- match proof with
- None -> assert false
- | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
+ let curi,metasenv,pbo,pty = proof in
let metano,context,ty =
- match goal with
- None -> assert false
- | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
+ List.find (function (m,_,_) -> m=goal) metasenv
in
let string_of_name =
function
| t -> t
) metasenv
in
- (Some (curi,metasenv',pbo,pty), goal)
+ (curi,metasenv',pbo,pty), [goal]