From 927d17d04d98e65cf19925915d24352c264065ae Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 25 Mar 2016 13:22:16 -0400 Subject: [PATCH] A fix for Coq 8.4 --- TypesAndMutation.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TypesAndMutation.v b/TypesAndMutation.v index a23638f..0eb2dc2 100644 --- a/TypesAndMutation.v +++ b/TypesAndMutation.v @@ -226,7 +226,7 @@ Module References. Ltac loopy := propositional; subst; simplify; repeat match goal with - | [ x : _ * _ |- _ ] => cases x; simplify + | [ x : (_ * _)%type |- _ ] => cases x; simplify end; propositional; subst; repeat match goal with