X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2FprimitiveTactics.ml;h=192460633d7577ff26a18e40d2d8ac4e8f699651;hb=92081320b50b03d6bf296552d2cae9e4b398f1be;hp=5fb8d4ae1eb56f88522cb14133c1a7c846a60e69;hpb=9e18c7f8aa6c5b905598521c769c1a2f58c13262;p=helm.git

diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index 5fb8d4ae1..192460633 100644
--- a/components/tactics/primitiveTactics.ml
+++ b/components/tactics/primitiveTactics.ml
@@ -419,8 +419,17 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
  =
   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 =
@@ -571,7 +580,7 @@ let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fres
 
 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) =