coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?

From: Georgi Guninski <guninski AT guninski.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?
Date: Wed, 25 May 2011 16:18:37 +0300
Header: best read with a sniffer

On Tue, May 24, 2011 at 04:05:47PM +0200, Pierre Corbineau wrote:
> It is a feature: AA is recognized as a 'logical connective' and is
> 'eagerly unfolded'.
>
> Pierre
>
thank you.

is this True or False, [firstorder] crashes with SEGV and i can't prove it:

Inductive CC : Prop := C1: (exists B : Prop,CC)->CC.

[Coq-Club] is it normal [firstorder] to hang on simple testcase?, Georgi Guninski
- Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Pierre Corbineau
  - Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Georgi Guninski
    - Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Jean-Francois Monin
      - Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Georgi Guninski
    - Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Pierre Corbineau
      - Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Georgi Guninski
        
        Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, David Baelde
        
        Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Georgi Guninski
        
        Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, David Baelde
        
        Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Alexandre Pilkiewicz
        
        Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Stéphane Glondu