Mercurial > cpdt > repo
diff src/Match.v @ 547:2c8c693ddaba
Fixes for Coq 8.6
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 12 Jul 2017 13:08:24 -0400 |
parents | 4f6e7bab0d45 |
children |
line wrap: on
line diff
--- a/src/Match.v Thu May 12 18:09:36 2016 -0500 +++ b/src/Match.v Wed Jul 12 13:08:24 2017 -0400 @@ -444,7 +444,7 @@ Sometimes we need to employ the opposite direction of "nonterminal escape," when we want to pass a complicated tactic expression as an argument to another tactic, as we might want to do in invoking %\coqdocvar{%#<tt>#map#</tt>#%}%. *) Goal False. - let ls := map (nat * nat)%type ltac:(fun x => constr:(x, x)) (1 :: 2 :: 3 :: nil) in + let ls := map (nat * nat)%type ltac:(fun x => constr:((x, x))) (1 :: 2 :: 3 :: nil) in pose ls. (** [[ l := (1, 1) :: (2, 2) :: (3, 3) :: nil : list (nat * nat)