pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

A fix for Coq 8.4

Browse source
This commit is contained in:
Adam Chlipala 2016-03-25 13:22:16 -04:00
parent f76a1055d8
commit 927d17d04d
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
TypesAndMutation.v
View file

@ -226,7 +226,7 @@ Module References.
Ltac loopy := propositional; subst; simplify; Ltac loopy := propositional; subst; simplify;
repeat match goal with repeat match goal with
| [ x : _ * _ |- _ ] => cases x; simplify | [ x : (_ * _)%type |- _ ] => cases x; simplify
end; end;
propositional; subst; propositional; subst;
repeat match goal with repeat match goal with