- Makefile update

[helm.git] / matita / components / ng_tactics / nDestructTac.ml

diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml
index daa80fd8f08690e2964db8e1469d5e21ca38f8c3..990cc672bbede15aaa17f8f9a2a088e8c452319e 100644 (file)
--- a/matita/components/ng_tactics/nDestructTac.ml
+++ b/matita/components/ng_tactics/nDestructTac.ml
@@ -471,7 +471,7 @@ let subst_tac ~context ~dir skip cur_eq =
       | _ -> cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in
     let varname = match var with
       | NCic.Rel var -> 
-          let name,_ = List.nth context var in
+          let name,_ = List.nth context (var+cur_eq-1) in
          HLog.warn (Printf.sprintf "destruct: trying to remove variable: %s" name);
          [name]
       | _ -> []
@@ -497,7 +497,7 @@ let subst_tac ~context ~dir skip cur_eq =
                  (* XXX: temo che la clear multipla funzioni bene soltanto se
                   * gli identificatori sono nell'ordine giusto.
                   * Per non saper né leggere né scrivere, usiamo due clear
-                  * invece di una *)              
+                  * invece di una *)
                  NTactics.try_tac (NTactics.clear_tac [eq_name]);
                 NTactics.try_tac (NTactics.clear_tac varname);
 ]@
@@ -712,7 +712,9 @@ let rec destruct_tac0 tags acc domain skip status goal =
     let has_cleared = 
      try 
        let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false
-     with _ -> true in
+     with 
+      | Sys.Break as e -> raise e
+      |_ -> true in
     let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
     let acc = rm_eq has_cleared acc in
     let skip = rm_eq has_cleared skip in
@@ -728,7 +730,9 @@ let rec destruct_tac0 tags acc domain skip status goal =
       let has_cleared = 
        try 
          let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false
-       with _ -> true in
+       with 
+         | Sys.Break as e -> raise e         
+        | _ -> true in
       let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
       let acc = rm_eq has_cleared acc in
       let skip = rm_eq has_cleared skip in