=
let module C = Cic in
let curi,metasenv,pbo,pty = proof in
=
let module C = Cic in
let curi,metasenv,pbo,pty = proof 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 =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let newmeta = new_meta_of_proof ~proof in
let fresh_name =
let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
let term = C.Sort C.Set in
let letout_tac (proof, goal) =
let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
let term = C.Sort C.Set in
let letout_tac (proof, goal) =