coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "named" goals with refine

From: Dmitry Grebeniuk <gdsfh1 AT gmail.com>
To: Guillaume Melquiond <coq-club AT inria.fr>
Subject: Re: [Coq-Club] "named" goals with refine
Date: Wed, 16 Jan 2013 11:44:13 +0200

Hello.

> match goal with
> | |- named _ "goal_nat" => unfold named ; omega
> | |- named _ "goal_bool" => unfold named ; apply bool_tf
> | _ => idtac
> end.

Thank you! It works, I will use this trick.

[Coq-Club] "named" goals with refine, Dmitry Grebeniuk, 01/16/2013
- Re: [Coq-Club] "named" goals with refine, Guillaume Melquiond, 01/16/2013
  - Re: [Coq-Club] "named" goals with refine, Dmitry Grebeniuk, 01/16/2013
- Re: [Coq-Club] "named" goals with refine, AUGER Cédric, 01/16/2013
  - Re: [Coq-Club] "named" goals with refine, Dmitry Grebeniuk, 01/16/2013
    - Re: [Coq-Club] "named" goals with refine, AUGER Cédric, 01/16/2013
- Re: [Coq-Club] "named" goals with refine, AUGER Cédric, 01/16/2013
  - Re: [Coq-Club] "named" goals with refine, Gabriel Scherer, 01/16/2013