Daniel R. Grayson

This is probably something about precision used while printing. ``` i3 : 2^53 o3 = 9007199254740992 i8 : (2^53-1) + 0. o8 = 9007199254740990 o8 : RR (of precision 53)...

Since the Style package has a Makefile created from its Makefile.in in its auxiliary files directory, "installPackage" was failing on it, because "copyDirectory" has a problem. Perhaps add an option...

notation declarations

1

If an operator is declared as a notation in two files with differing level or associativity, then the two files cannot both be imported because of the conflict. To fix...

Notation such as ``` Local Notation "[]" := nil (at level 0, format "[]"). Local Infix "::" := cons. ``` in Lists.v should be made non-local and put into a...

add links

2

I'll add some links to Vladimir's discussions of UniMath to the file README.md, including: https://www.newton.ac.uk/seminar/20170710113012301 (the slides and video are both there) https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2016_09_22_HLF_Heidelberg.pdf https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/4th%20HLF%20-%20Lecture%20Vladimir%20Voevodsky.mp4 https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2016_07_14_Berlin_ICMS_short.pdf Are there others?

company-coq

1

Mention company-coq in the README, see https://github.com/UniMath/UniMath/pull/447#issuecomment-248075105

complicated `intros` patterns

10

Complicated patterns with `intros` will stop working the same way in the latest version of Coq on the trunk. To see an example of how I've had to fix some,...

readme

15

`~/src/M2/M2.git/M2/distributions/dmg/ReadMe-MacOSX.rtf` recommends aquamacs, but "emacs for mac os x" from https://emacsformacosx.com/ is just as good, if not better, and should be mentioned on an equal footing.

associativity of implication

2

The associativity of implication, `A ⇒ B`, is wrong, since it differs from that of `A -> B`. ``` Reserved Notation "A ⇒ B" (at level 95, no associativity). (*...

decidable propositions

1

Here are some definitions from Foundations concerning decidable propositions: ``` Lemma isdecpropif ( X : UU ) : isaprop X -> ( coprod X ( neg X ) ) ->...