Omega: for non-arithmetical goals, try proving False from context (wish #2236)

 This way, no more error messages like "Unrecognized predicate".
 Some code simplification and reorganization on the way, in particular
 a few tests like "is_Prop ..." or "closed0 ..." were actually useless.
 Also add support for the situation H:~Zne x y for uniformity.

 Beware: scripts relying negatively on the strength of omega may have to
 be adapted (e.g. "try omega. some_more_tactics_in_case_omega_fails.").
 For instance, one line deletion in PermutSetoid.v
 Probably more cumbersome : "auto with *" becomes stronger since it
 may call omega. Todo : check the impact on contribs tomorrow.

 Btw, this commit seems to solve a bug where omega was to be guided
 by some (set foo:= ...) before being able to succeed (cf PermutSetoid.v)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14474 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 540b3fe30d..d0931f897f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -44,6 +44,8 @@ Tactics
 - Tactic autorewrite does no longer instantiate pre-existing
   existential variables (theoretical source of possible incompatibility).
 - Tactic "dependent rewrite" now supports equality in "sig".
+- Tactic omega now understands Zpred (wish #1912) and can prove any goal
+  from a context containing an arithmetical contradiction (wish #2236).
 
 Vernacular commands