X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FprimitiveTactics.ml;h=e09f0a1f7dc890ecbee234b53042677fea3aab91;hb=ae1827aaba945a25bdc209ca23aa836befa4bead;hp=9baf829ea940d2bad3c61d71ebfdea8781043f34;hpb=45d71beffd253ffd767a9afbfcec5c4f44afd8a8;p=helm.git diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index 9baf829ea..e09f0a1f7 100644 --- a/components/tactics/primitiveTactics.ml +++ b/components/tactics/primitiveTactics.ml @@ -246,14 +246,14 @@ let rec count_prods context ty = Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t | _ -> 0 -let apply_tac_verbose_with_subst ~term (proof, goal) = +let apply_with_subst ~term ~subst (proof, goal) = (* Assumption: The term "term" must be closed in the current context *) let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in let (_,metasenv,_,_) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let newmeta = new_meta_of_proof ~proof in + let newmeta = CicMkImplicit.new_meta metasenv subst in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = match term with C.Var (uri,exp_named_subst) -> @@ -326,10 +326,10 @@ let apply_tac_verbose_with_subst ~term (proof, goal) = (* ALB *) -let apply_tac_verbose_with_subst ~term status = +let apply_with_subst ~term ?(subst=[]) status = try (* apply_tac_verbose ~term status *) - apply_tac_verbose_with_subst ~term status + apply_with_subst ~term ~subst status (* TODO cacciare anche altre eccezioni? *) with | CicUnification.UnificationFailure msg @@ -338,7 +338,7 @@ let apply_tac_verbose_with_subst ~term status = (* ALB *) let apply_tac_verbose ~term status = - let subst, status = apply_tac_verbose_with_subst ~term status in + let subst, status = apply_with_subst ~term status in (CicMetaSubst.apply_subst subst), status let apply_tac ~term status = snd (apply_tac_verbose ~term status) @@ -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 =