Semantics of try changed (fixed) when applied to multiple goals that can now

fail independently.

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 0420c8119f2d6d9733e66e7799eb382e4ed874da..a9a46e7431dfe931b872edc4f4b8188ec68458b6 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -377,7 +377,7 @@ let eval_ng_tac tac =
   | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
   | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac 
   | GrafiteAst.NTry (_,tac) -> NTactics.try_tac
-      (aux f (text, prefix_len, tac))
+      (f f (text, prefix_len, tac))
   | GrafiteAst.NAssumption _ -> NTactics.assumption_tac
   | GrafiteAst.NBlock (_,l) -> 
       NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)

diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml
index 577edf9d903a889fd536aca8e127bbee60f717f4..c80fbc5569038d0bdeb405983c76fad3b10e54cb 100644 (file)
--- a/matita/components/ng_tactics/nTactics.ml
+++ b/matita/components/ng_tactics/nTactics.ml
@@ -261,10 +261,13 @@ let repeat_tac t s =
 
 
 let try_tac tac status =
+ let try_tac status =
   try
     tac status
   with NTacStatus.Error _ ->
     status
+ in
+  atomic_tac try_tac status
 ;;
 
 let first_tac tacl status =

diff --git a/matita/components/ng_tactics/nTactics.mli b/matita/components/ng_tactics/nTactics.mli
index bfa965391088cf484d82e5f73786618ca263e4eb..d9964ddcebbbd94f5b08b224f7792e36d294d4a0 100644 (file)
--- a/matita/components/ng_tactics/nTactics.mli
+++ b/matita/components/ng_tactics/nTactics.mli
@@ -23,7 +23,7 @@ val merge_tac: 's NTacStatus.tactic
 val focus_tac: int list -> 's NTacStatus.tactic
 val unfocus_tac: 's NTacStatus.tactic
 val skip_tac: 's NTacStatus.tactic
-val try_tac: 's NTacStatus.tactic -> 's NTacStatus.tactic
+val try_tac: NTacStatus.tac_status NTacStatus.tactic -> 's NTacStatus.tactic
 val repeat_tac: NTacStatus.tac_status NTacStatus.tactic -> 's NTacStatus.tactic
 
 val compare_statuses : past:#NTacStatus.lowtac_status -> present:#NTacStatus.lowtac_status -> int list * int list