From c5857506019a9c176753012fe97ff33b7a1e7f2a Mon Sep 17 00:00:00 2001 From: courant Date: Wed, 2 Oct 2002 15:39:32 +0000 Subject: Changements Omega git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3069 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGES b/CHANGES index 2c3d1d441a..f7a71e2bf5 100644 --- a/CHANGES +++ b/CHANGES @@ -43,6 +43,10 @@ Tactics - "Inversion" now applies also on quantified hypotheses (naming as for Intros until) - NewDestruct now accepts terms with missing hypotheses +- Omega could solve goals such as ~`x=y` but failed when the + hypothesis was unfolded to `x < y` -> False. This is fixed. In addition, + it can also recognize 'False' in the hypothesis and use it to solve the + goal. Miscellaneous -- cgit v1.2.3