Update build process to use COQPATH & _CoqProject

Removed all of the files not built by default; they can be resurrected from git
history.  _CoqProject is the standard way to list the files in a project and to
give information to coq_makefile.  COQPATH is the standard way to make use of
not-yet-installed libraries that are not part of your project (i.e., you don't
want to remove them when you `make clean`, etc.).

1 files changed, 0 insertions, 28 deletions

diff --git a/src/Assembly/DSL.v b/src/Assembly/DSL.v
deleted file mode 100644
index 2cb07a5d4..000000000
--- a/src/Assembly/DSL.v
+++ /dev/null
@@ -1,28 +0,0 @@
-
-Require Export ConstrainedComputation.
-
-Notation "const A" := CConst A.
-Notation "var A" := CVar A.
-Notation "A : B" := CJoin A B.
-Notation "left A" := CLeft A.
-Notation "right A" := CRight A.
-
-Notation "~ A" := UnaryExpr CNot A.
-Notation "- A" := UnaryExpr COpp A.
-Notation "A + B" := BinaryExpr CPlus A B.
-Notation "A - B" := BinaryExpr CMinus A B.
-Notation "A * B" := BinaryExpr CMult A B.
-Notation "A / B" := BinaryExpr CDiv A B.
-Notation "A & B" := BinaryExpr CAnd A B.
-Notation "A | B" := BinaryExpr COr A B.
-Notation "A ^ B" := BinaryExpr CXor A B.
-Notation "A >> B" := BinaryExpr CRShift A B.
-Notation "A << B" := BinaryExpr CLShift A B.
-
-Definition toExpr {type} (term: CTerm type) = TermExpr term.
-Coersion toExpr: {type} CTerm type >-> CExpr type.
-
-Notation "ret A" := CRet A
-Notation "A . B" := CCompose A B
-Notation "A ? B : C" := CIte A B C
-Notation "set A to B in C" := CLet A B C