coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] obligations

From: Daniel Schepler <dschepler AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] obligations
Date: Mon, 9 May 2016 17:38:17 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=dschepler AT gmail.com; spf=Pass smtp.mailfrom=dschepler AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f174.google.com
Ironport-phdr: 9a23:6/P4RBCKXTVXmYv3YH2SUyQJP3N1i/DPJgcQr6AfoPdwSP78psbcNUDSrc9gkEXOFd2CrakU2qyP6Ou7BSQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTmkbnpsMaPKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WZgyWrlAYT29exhFPGk3O6Azwdpb3qCrz8ORnjnq0J8rzGJw9XzWv6+9QQx/lkCMKLXZt/HrcisFoiK9BiB2krh17hYXTZdfGZ7JFYqrBcIZCFiJ6VcFLWnkEW9vkYg==

On Mon, May 9, 2016 at 4:32 PM, Vadim Zaliva
<vzaliva AT cmu.edu>
wrote:
> I am having some trivial problems with solving obligations under 8.5. It
> goes like this:
>
> Obligation Tactic := ring.

My guess would be you need "Obligation Tactic := program_simpl; ring."
That would have it perform the same simplifications that "Next
Obligation." performs before showing you the problem.
--
Daniel Schepler

[Coq-Club] obligations, Vadim Zaliva, 05/10/2016
- Re: [Coq-Club] obligations, Matthieu Sozeau, 05/10/2016
- Re: [Coq-Club] obligations, Daniel Schepler, 05/10/2016
  - Re: [Coq-Club] obligations, Vadim Zaliva, 05/10/2016
    - Re: [Coq-Club] obligations, Vadim Zaliva, 05/10/2016
      - Re: [Coq-Club] obligations, Matthieu Sozeau, 05/10/2016
        
        Re: [Coq-Club] obligations, Vadim Zaliva, 05/11/2016
        
        Re: [Coq-Club] obligations, Vadim Zaliva, 05/12/2016
        
        Re: [Coq-Club] obligations, Matthieu Sozeau, 05/12/2016