=
let module C = Cic in
let curi,metasenv,pbo,pty = proof in
+ (* occur check *)
+ let occur i t =
+ let m = CicUtil.metas_of_term t in
+ List.exists (fun (j,_) -> i=j) m
+ in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let _,_ = (* TASSI: FIXME *)
+ if occur metano term then
+ raise
+ (ProofEngineTypes.Fail (lazy
+ "You can't letin a term containing the current goal"));
+ let _,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let newmeta = new_meta_of_proof ~proof in
let fresh_name =
module C = Cic
-let letout_tac () =
+let letout_tac =
let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
let term = C.Sort C.Set in
let letout_tac (proof, goal) =