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

0 files changed, 0 insertions, 0 deletions