Fight namespace pollution

[andres-erbsen]

This is on top of #8.

• examples moved into FCF/ because that name would almost definitely have collisions
• central Makefile and _CoqProject, individual parts of the repository can be built using make -f Makefile.coq src/FCF/FCF.v
  • run make update-_CoqProject after git add or git rm or git mv
  • no more make install in the main Makefile -- it can still be used directly from Makefile.coq, but I would recommend against that anyway.
• removed non-building files (may one go to git history if they want to port them)
  • alternatiely, we could keep them in the repo and exclude them through some other means?
• merged the two readme files and updated build and usage instructions
• no more .dir-locals.el (this drops support for outdated versions of ProofGeneral)

[andres-erbsen]

I'm not sure what github is saying about merge conflicts -- this merges cleanly on my machine.

[adampetcher]

I would prefer to keep the non-building files in the repo for the following reasons:

1. They still can be useful illustrations (especially the examples).
2. There may be some argument in there that is needed in the future, and it would be easier to fix the file than to develop it from scratch. A person probably wouldn't think to look in the history for "almost working" theory.

That being said, some of the non-building files are definitely old junk that needs to be removed. So I suggest:

1. Leave these files in and exclude them from the build. If you like, you can move the non-building files to a separate directory to simplify the build.
2. Create a ticket (assigned to me) reminding me to go through and clean up these broken files. Useless ones should be removed, valuable ones should be fixed.
3. If you like, you can remove the entire ESPADA directory. I don't plan to maintain this proof. If you do this, create a ticket (assigned to me) reminding me to look through this proof and see if there is any useful theory that should be extracted.

Everything else looks great! You got a merge conflict because I (very) recently changed a file that you moved. It should be trivial to resolve after you pull the latest.

[adampetcher]

See comment on deleted files.

[andres-erbsen]

I removed ESPADA (issue #11).

These files build now:

     src/FCF/examples/Commit.v
     src/FCF/Class.v
     src/FCF/ExpectedPolyTime.v
     src/FCF/RndDup.v

I was unable to fully fix the following files (issue #12):

    src/FCF/Broken/Encryption_2W.v
    src/FCF/Broken/ListHybrid.v
    src/FCF/Broken/Procedure.v
    src/FCF/Broken/RandPermSwitching.v
    src/FCF/Broken/Sigma.v
    src/FCF/Broken/State.v
    src/FCF/examples/EC_DRBG.v

These files are still built. But significant chunks of their content are commented out and admitted.

[adampetcher]

Nice work. Thanks!