coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "Error: refine: proof term contains metas in a product."

From: Anders Lundstedt <anders AT anderslundstedt.se>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] "Error: refine: proof term contains metas in a product."
Date: Sun, 16 Feb 2014 16:46:16 +0100

On Sun, Feb 16, 2014 at 8:50 AM, Arnaud Spiwack
<aspiwack AT lix.polytechnique.fr>
wrote:
> ... Except moving to the development
> version of Coq: the refine tactic has been completely reimplemented and
> accepts holes anywhere.

Is it possible to just add the reimplented refine tactic as a custom
tactic, without too much fuss?

[Coq-Club] "Error: refine: proof term contains metas in a product.", Anders Lundstedt, 02/16/2014
- Re: [Coq-Club] "Error: refine: proof term contains metas in a product.", Arnaud Spiwack, 02/16/2014
  - Re: [Coq-Club] "Error: refine: proof term contains metas in a product.", Anders Lundstedt, 02/16/2014
    - Re: [Coq-Club] "Error: refine: proof term contains metas in a product.", Jason Gross, 02/16/2014
      - Re: [Coq-Club] "Error: refine: proof term contains metas in a product.", Anders Lundstedt, 02/16/2014
    - Re: [Coq-Club] "Error: refine: proof term contains metas in a product.", Arnaud Spiwack, 02/16/2014