benediktahrens/rezk_completion — pull request #1 by DanGrayson (2013-10-30 15:20:15+00:00)
Title: Reorganize the files into two subdirectories

This will make it possible for the Rezk Completion files to be used with
another version of the Foundations files of Voevodsky. (The problem is that
coq doesn't like to find a file such as 'uuu.v' occurring twice in directories
of the search path.) The advantages are: that a developer of the Foundations
files can easily verify that the Rezk Completion proof continues works; and
that a developer of a subsequent proof can incorporate all of the Foundations
files as well as the Rezk Completion proof.

Comments have been inserted into the file 'Make' to illustrate an alternative
usage.