search

jesper-bengtson / Charge

Higher-order separation logic framework in Coq
Other
1 stars 1 forks source link

Building Charge under a library name #1

Open gmalecha opened 10 years ago

gmalecha commented 10 years ago

Can Charge! be built under a library name to prevent name collisions with other projects?

Here is a patch

diff --git a/Charge!/KopitiamMakefile b/Charge!/KopitiamMakefile
index 342d76d..d3d5a71 100644
--- a/Charge!/KopitiamMakefile
+++ b/Charge!/KopitiamMakefile
@@ -4,11 +4,8 @@ COQFLAGS = -noglob

 bin/%.vo: src/%.v
        $(_COQCMD)
-override COQFLAGS += -R "src" ""
-override COQFLAGS += -R "bin" ""
-override COQFLAGS += -R "/Users/jebe/coqs/coq-8.4pl2/theories" "Coq"
-override COQFLAGS += -R "/Users/jebe/coqs/coq-8.4pl2/plugins" "Coq"
-override COQFLAGS += -R "/Users/jebe/coqs/coq-8.4pl2/user-contrib" ""
+override COQFLAGS += -R "src" -as "Charge"
+override COQFLAGS += -R "bin" -as "Charge"
 OBJECTS = \
        bin/Logics/BILInsts.vo \
        bin/Logics/BILogic.vo \
gmalecha commented 10 years ago

In addition to this, all references to Charge files should use the fully qualified names. This will make things work nicely when the module problems are fixed in the next version of Coq.