The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Thanks for Sean and Edsko for solutions,

Anyway, Sean asked me for example and here is one very simple:

Coq < Parameter valid_prop : Prop.
valid_prop is assumed

Coq < Require Import Omega.

Coq < Goal 2>100 -> valid_prop.
1 subgoal

  ============================
   2 > 100 -> valid_prop

Unnamed_thm < intro.
1 subgoal

  H : 2 > 100
  ============================
   valid_prop

Unnamed_thm < omega.
Toplevel input, characters 0-5
> omega.
> ^^^^^
User error: Omega: Unrecognized atomic proposition: valid_prop

Marko Malikoviæ