From a2aa673e87859464be0ae57841b1313701dbe912 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 1 Jan 2009 09:27:27 +0000 Subject: Update git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11730 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index cd8ac1562..0e7eb9397 100644 --- a/CHANGES +++ b/CHANGES @@ -3,10 +3,13 @@ Changes since V8.2 Tactics -- "discriminate" now performs intros before trying to discriminate an +- Tactic "discriminate" now performs intros before trying to discriminate an hypothesis of the goal (previously it applied intro only if the goal had the form t1<>t2). -- rewrite now supports rewriting on ad hoc equalities such as eq_true. +- Tactic "rewrite" now supports rewriting on ad hoc equalities such as eq_true. +- Tactic "intuition" now preserves inner "iff" (exceptional source of + incompatibilities solvable by redefining "intuition" as + "unfold iff in *; intuition". Tools @@ -14,6 +17,11 @@ Tools e.g. to globally update notations). - New tool beautify-archive to beautify a full archive of developments. +Library + +- Use "Coq standard" names for the properties of eq and identity + (e.g. refl_equal is now eq_refl). Support for compatibility is provided. + Changes from V8.1 to V8.2 ========================= @@ -304,9 +312,6 @@ Tactics - New tactic "instantiate" (without argument). - Tactic firstorder "with" and "using" options have their meaning swapped for consistency with auto/eauto (source of incompatibility). -- Tactic "intuition" now preserves inner "iff" (exceptional source of - incompatibilities solvable by redefining "intuition" as - "unfold iff in *; intuition". - Tactic "generalize" now supports "at" options to specify occurrences and "as" options to name the quantified hypotheses. - New tactic "specialize H with a" or "specialize (H a)" allows to transform -- cgit v1.2.3