Notes to self while learning to use Coq, the proof assistant language.
Set Printing Allto remove the syntactic sugar. However this can potentially make things horribly difficult to read, so beware.
makemay fail and trying to import may give you a directory missing error:
Error: Unable to locate library yourFileToImport. Makefile:270: recipe for target 'yourCurrentFileThatImports.vo' failed
coqc -Q . LF yourFileToImport.vin the command line and then when importing, do
Require Export LF.yourFileToImport.