From 3ace6e853d2cb8ce8c98b7d8c07a4f6c6b61ba84 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 3 Dec 2010 22:52:49 +0000 Subject: [PATCH] Semantics of try changed (fixed) when applied to multiple goals that can now fail independently. --- matita/components/grafite_engine/grafiteEngine.ml | 2 +- matita/components/ng_tactics/nTactics.ml | 3 +++ matita/components/ng_tactics/nTactics.mli | 2 +- 3 files changed, 5 insertions(+), 2 deletions(-) diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 0420c8119..a9a46e743 100644 --- 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 577edf9d9..c80fbc556 100644 --- 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 bfa965391..d9964ddce 100644 --- 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 -- 2.39.2