- destruct tactic: automatic simplification in case of failure removed

[helm.git] / components / tactics / destructTactic.ml

diff --git a/components/tactics/destructTactic.ml b/components/tactics/destructTactic.ml
index 1344e978fb0bafdf256fdec7593ddc257d842c2e..ea871a0d4aff09e491194cf03d1dbf33ad0650b2 100644 (file)
--- 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