caryoscelus/agda: My dev branches of agda (i.e. mostly a mirror) @ js_amd

Ulf Norell 988141b7e8 [ primitive ] changed primitive integers to a datatype		9 lat temu
..
highlighting	988141b7e8 [ primitive ] changed primitive integers to a datatype	9 lat temu
Literate.lagda	c92b799692 Files given on the command line must now be on the include path.	15 lat temu