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

Update for Coq 8.12.2

Browse source
This commit is contained in:
Adam Chlipala 2021-01-03 14:56:39 -05:00
parent 845c9189c1
commit f14d064555
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
DataAbstraction.v
View file

@ -629,7 +629,7 @@ Module AlgebraicWithEquivalenceRelation.
equality. equality.
unfold equiv, elements. unfold equiv, elements.
simplify. simplify.
SearchAbout app cons nil. Search app cons nil.
apply app_inj_tail. apply app_inj_tail.
rewrite <- app_assoc. rewrite <- app_assoc.
rewrite <- app_assoc. rewrite <- app_assoc.
@ -1547,7 +1547,7 @@ Module NatRangeSet <: FINITE_SET with Definition key := nat.
unfold member, add; simplify. unfold member, add; simplify.
cases s. cases s.
SearchAbout Compare_dec.leb. Search Compare_dec.leb.
rewrite Compare_dec.leb_correct. rewrite Compare_dec.leb_correct.
equality. equality.
linear_arithmetic. linear_arithmetic.