From 453dd2bc6eb24296530b2557628472d4296704e8 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 14 Jan 2015 11:27:17 +0100 Subject: CHANGES: my recent updates to Ltac. - gfail - multimatch - tryif/then/else --- CHANGES | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CHANGES b/CHANGES index b5b379eca8..4a9c3a40d8 100644 --- a/CHANGES +++ b/CHANGES @@ -118,6 +118,9 @@ Tactics the need of the undocumented "constructor " syntax which is now equivalent to "once (constructor; tac)". (potential source of rare incompatibilities). + * New "multimatch" variant of "match" tactic which backtracks to + new branches in case of a later failure. The "match" tactic is + equivalent to "once multimatch". * New selector all: to qualify a tactic allows applying a tactic to all the focused goal, instead of just the first one as is the default. @@ -140,6 +143,8 @@ Tactics Accompanied by "guard" tactic which fails if a Boolean test does not pass. * New tactical "[> ... ]" to apply tactics to individual goals. + * New tactic "gfail" which works like "fail" except it will also + fail if every goal has been solved. * The refine tactic is changed not to use an ad hoc typing algorithm to generate subgoals. It also uses the dependent subgoal feature to generate goals to materialize every existential variable which @@ -156,6 +161,8 @@ Tactics - Matching using "lazymatch" was fundamentally modified. It now behaves like "match" (immediate execution of the matching branch) but without the backtracking mechanism in case of failure. +- New "tryif t then u else v" tactical which executes "u" in case of success + of "t" and "v" in case of failure. - New conversion tactic "native_compute": evaluates the goal (or an hypothesis) with a call-by-value strategy, using the OCaml native compiler. Useful on very intensive computations. -- cgit v1.2.3