Removed Demo.v from _CoqProject

monadius · monadius · commit 4e11126bb244 · 2019-07-13T11:57:26.000-07:00
diff --git a/README.md b/README.md
@@ -49,4 +49,10 @@ Run `make .merlin` to create the `.merlin` file.
 ## Examples
 
 See [theories/Demo.v](theories/Demo.v) and [theories/Demo2.v](theories/Demo2.v)
-for more examples.
+for more examples.
+
+Compiling demo files:
+```
+coqc -I src -R theories/ CW theories/Demo.v
+coqc -I src -R theories/ CW theories/Demo2.v
+```
diff --git a/_CoqProject b/_CoqProject
@@ -2,7 +2,6 @@
 -I src
 
 theories/Loader.v
-theories/Demo.v
 
 src/coq_cw.ml
 src/coq_cw.mli
diff --git a/_CoqProjectDemo b/_CoqProjectDemo
@@ -0,0 +1,10 @@
+-R theories/ CW
+-I src
+
+theories/Loader.v
+theories/Demo.v
+
+src/coq_cw.ml
+src/coq_cw.mli
+src/g_coq_cw.ml4
+src/coq_cw_plugin.mlpack
diff --git a/cw_example/build.sh b/cw_example/build.sh
@@ -0,0 +1,3 @@
+coqc preloaded.v
+coqc solution.v
+coqc -I ../src -Q ../theories CW test.v
diff --git a/cw_example/preloaded.v b/cw_example/preloaded.v
@@ -0,0 +1 @@
+Axiom test_axiom : False.
diff --git a/cw_example/solution.v b/cw_example/solution.v
@@ -0,0 +1,4 @@
+Require Import preloaded.
+
+Lemma solution : 1 + 1 = 3.
+Proof. firstorder using test_axiom. Qed.
diff --git a/cw_example/test.v b/cw_example/test.v
@@ -0,0 +1,6 @@
+Require solution.
+Require Import preloaded.
+From CW Require Import Loader.
+
+CWTest "Testing solution" solution.solution Assumes test_axiom.
+
