let clearbody ~hyp =
let clearbody (proof, goal) =
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,_,_ = CicUtil.lookup_meta goal metasenv in
let string_of_name =
function
(fun entry context ->
match entry with
Some (C.Name hyp',C.Def (term,ty)) when hyp = hyp' ->
- let cleared_entry =
- let ty =
- match ty with
- Some ty -> ty
- | None ->
- fst
- (CicTypeChecker.type_of_aux' metasenv context term
- CicUniv.empty_ugraph) (* TASSI: FIXME *)
- in
- Some (C.Name hyp, Cic.Decl ty)
- in
+ let cleared_entry = Some (C.Name hyp, Cic.Decl ty) in
cleared_entry::context
| None -> None::context
- | Some (n,C.Decl t)
- | Some (n,C.Def (t,None)) ->
+ | Some (n,C.Decl t) ->
let _,_ =
try
CicTypeChecker.type_of_aux' metasenv context t
- CicUniv.empty_ugraph (* TASSI: FIXME *)
+ CicUniv.oblivion_ugraph (* TASSI: FIXME *)
with
_ ->
raise
))
in
entry::context
- | Some (_,Cic.Def (_,Some _)) -> assert false
+ | Some (n,Cic.Def (te,ty)) ->
+ (try
+ ignore
+ (CicTypeChecker.type_of_aux' metasenv context te
+ CicUniv.oblivion_ugraph (* TASSI: FIXME *));
+ ignore
+ (CicTypeChecker.type_of_aux' metasenv context ty
+ CicUniv.oblivion_ugraph (* TASSI: FIXME *));
+ with
+ _ ->
+ raise
+ (PET.Fail
+ (lazy ("The correctness of hypothesis " ^
+ string_of_name n ^
+ " relies on the body of " ^ hyp)
+ )));
+ entry::context
) canonical_context []
in
let _,_ =
try
CicTypeChecker.type_of_aux' metasenv canonical_context' ty
- CicUniv.empty_ugraph (* TASSI: FIXME *)
+ CicUniv.oblivion_ugraph (* TASSI: FIXME *)
with
_ ->
raise
| t -> t
) metasenv
in
- (curi,metasenv',pbo,pty, attrs), [goal]
+ (curi,metasenv',_subst,pbo,pty, attrs), [goal]
in
PET.mk_tactic clearbody
let clear_one ~hyp =
let clear_one (proof, goal) =
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty =
CicUtil.lookup_meta goal metasenv
in
(true, None::context)
| None -> (b, None::context)
| Some (n,C.Decl t)
- | Some (n,Cic.Def (t,Some _))
- | Some (n,C.Def (t,None)) ->
+ | Some (n,Cic.Def (t,_)) ->
if b then
let _,_ =
try
CicTypeChecker.type_of_aux' metasenv context t
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
with _ ->
raise
(PET.Fail
let _,_ =
try
CicTypeChecker.type_of_aux' metasenv canonical_context' ty
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
with _ ->
raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
in
| t -> t
) metasenv
in
- (curi,metasenv',pbo,pty, attrs), [goal]
+ (curi,metasenv',_subst,pbo,pty, attrs), [goal]
in
PET.mk_tactic clear_one
try List.combine froms tos
with Invalid_argument _ -> raise (PET.Fail (lazy error))
in
- let curi, metasenv, pbo, pty, attrs = proof in
+ let curi, metasenv, _subst, pbo, pty, attrs = proof in
let metano, _, _ = CicUtil.lookup_meta goal metasenv in
let rename_map = function
| Some (Cic.Name hyp, decl_or_def) as entry ->
| conjecture -> conjecture
in
let metasenv = List.map map metasenv in
- (curi, metasenv, pbo, pty, attrs), [goal]
+ (curi, metasenv, _subst, pbo, pty, attrs), [goal]
in
PET.mk_tactic rename
-
-let set_goal n =
- PET.mk_tactic
- (fun (proof, goal) ->
- let (_, metasenv, _, _, _) = proof in
- if CicUtil.exists_meta n metasenv then
- (proof, [n])
- else
- raise (PET.Fail (lazy ("no such meta: " ^ string_of_int n))))