Subject: Ssreflect Users Discussion List
List archive
- From: Jean-Jacques Levy <>
- To:
- Subject: ssr 1.2 vs ssr 1.3
- Date: Fri, 17 Jun 2011 17:58:40 +0200
Dear ssreflecters,
Ltac move_to_top x :=match reverse goal with| H : _ |- _ => try move x after Hend.
is ok with release 1.2, but fails with 1.3:
Error: Intro pattern x not allowed here
Help! -JJ-
- ssr 1.2 vs ssr 1.3, Jean-Jacques Levy, 06/17/2011
- RE: ssr 1.2 vs ssr 1.3, Georges Gonthier, 06/17/2011
- Re: ssr 1.2 vs ssr 1.3, Enrico Tassi, 06/17/2011
- RE: ssr 1.2 vs ssr 1.3, Georges Gonthier, 06/17/2011
Archive powered by MHonArc 2.6.18.