Ssreflect Users Discussion List

[François Pottier <>]

Hello,

Once ssreflect is loaded, the tactic "omega" no longer works out of the box
(see attached file for an example). Is there a simple way of expanding away
all of ssreflect's notations and definitions, so that "omega" works again?

Thanks,

--
François Pottier

http://gallium.inria.fr/~fpottier/

Require Import Omega.

Goal
  forall x y,
  x < y ->
  x < y + 1.
Proof.
  intros. omega.
Qed.

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Goal
  forall x y,
  x < y ->
  x < y + 1.
Proof.
  intros. omega.
Qed.