X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FdestructTactic.ml;fp=components%2Ftactics%2FdestructTactic.ml;h=ea871a0d4aff09e491194cf03d1dbf33ad0650b2;hb=5aa4da5846c72942f3d204f71ecfba8d6cc7911b;hp=1344e978fb0bafdf256fdec7593ddc257d842c2e;hpb=f1efdff5ded26d264f2848ff53c19fe2099682a3;p=helm.git

diff --git a/components/tactics/destructTactic.ml b/components/tactics/destructTactic.ml
index 1344e978f..ea871a0d4 100644
--- a/components/tactics/destructTactic.ml
+++ b/components/tactics/destructTactic.ml
@@ -484,7 +484,7 @@ and subst_tac ~lterm ~direction ~where ~continuation =
    in
    PET.mk_tactic subst_tac
 
-and destruct ?(simplified = false) ~first_time term =
+and destruct ~first_time term =
  let are_convertible hd1 hd2 metasenv context = 
    fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph)
  in
@@ -574,17 +574,11 @@ and destruct ?(simplified = false) ~first_time term =
 	    | _, C.Rel i2 when DTI.does_not_occur i2 t1 ->
 	       mk_subst_chain `RightToLeft i2 t1 t2
 (* else part *)
-	    | _ when first_time && simplified -> raise exn_nothingtodo
-	    | _ when simplified (* && not first time *) -> T.id_tac
-            | _ (* when not simplified *) -> 
-               T.then_ ~start:(simpl_in_term context term)
-                       ~continuation:(destruct ~simplified:true ~first_time term)
+	    | _ when first_time -> raise exn_nothingtodo
+	    | _ (* when not first time *) -> T.id_tac
            end
-     | _ when first_time && simplified -> raise exn_nothingtodo
-     | _ when simplified (* && not first time *) -> T.id_tac
-     | _ (* when not simplified *) -> 
-        T.then_ ~start:(simpl_in_term context term)
-                ~continuation:(destruct ~simplified:true ~first_time term)
+     | _ when first_time -> raise exn_nothingtodo
+     | _ (* when not first time *) -> T.id_tac
   in  
     PET.apply_tactic tac status
  in