The Coq mailing list

[Brian Emre Aydemir <baydemir AT cis.upenn.edu>]

Ah, I see.  Out of curiosity, is the casetype tactic similar to the 
elimtype tactic?  It looks like the reference manual doesn't say 
anything about casetype (or maybe I'm just looking in the wrong 
places).

Thanks,
Brian

On 2004 Oct 18, at 07:29, Claude Marche wrote:

> I guess the Omega module adds some new hints in the zarith hint base,
> and as for any other module, it may or may not be clearly documented.
>
> Anyway, to make the omega tactic solve your goal when hypotheses are
> inconsistant, you could do
>
> casetype False; omega.
>
> - Claude
>
> > > > > > "Brian" == Brian Emre Aydemir 
> > > > > > <baydemir AT cis.upenn.edu>
> > > > > >  writes:
>
>     Brian> Hi,
>     Brian> I have noticed the following behavior about the Omega 
> module.
>     Brian> Sometimes I have a subgoal where the equality is a 
> conclusion on
>     Brian> something other than terms of type nat or Z, and where the 
> hypotheses
>     Brian> include (n < k) and (n >= k) for n and k arbitrary natural 
> numbers (a
>     Brian> contradiction that makes the subgoal trivially true).

--
Brian Emre Aydemir
http://www.cis.upenn.edu/~baydemir/