From 8a701c74a1fd3d05fefe48e6129c59793c5d611c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 17 Jun 2016 16:38:57 +0200
Subject: fix parsing (coq trunk goal selector/ltac:)

---
 mathcomp/ssrtest/first_n.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssrtest/first_n.v b/mathcomp/ssrtest/first_n.v
index 2cb6c32..3d99a0f 100644
--- a/mathcomp/ssrtest/first_n.v
+++ b/mathcomp/ssrtest/first_n.v
@@ -5,7 +5,7 @@ From mathcomp
 Require Import ssrbool.
 
 Lemma test : False -> (bool -> False -> True -> True) -> True.
-move=> F; let w := 2 in apply; last w first.
+move=> F; let w := constr:(2) in apply; last w first.
 - by apply: F.
 - by apply: I.
 by apply: true.
-- 
cgit v1.2.3