Use "-as" to put CompCert modules in a compcert.xxx namespace.

Simplified the scripts "coq" and "pg".
Updated deps.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 11 insertions, 4 deletions

diff --git a/pg b/pg
index 9242303..33a70ce 100755
--- a/pg
+++ b/pg
@@ -4,9 +4,7 @@
 # Recompile the modified file after coqide editing
 
 PWD=`pwd`
-ARCH=$PWD/`sed -n -e 's/^ARCH=//p' Makefile.config`
-VARIANT=$ARCH/`sed -n -e 's/^VARIANT=//p' Makefile.config`
-
+INCLUDES=`make print-includes`
 
 make -q ${1}o || {
   make -n ${1}o | grep -v "\\b${1}\\b" | \
@@ -14,9 +12,18 @@ make -q ${1}o || {
     sh -c "$cmd" || exit 2
    done)
 }
+
 COQPROGNAME="coqtop"
-COQPROGARGS="\"-I\" \"$PWD/lib\" \"-I\" \"$PWD/common\" \"-I\" \"$VARIANT\" \"-I\" \"$ARCH\" \"-I\" \"$PWD/backend\" \"-I\" \"$PWD/cfrontend\" \"-I\" \"$PWD/flocq\" \"-I\" \"$PWD/flocq/Appli\" \"-I\" \"$PWD/flocq/Calc\" \"-I\" \"$PWD/flocq/Core\" \"-I\" \"$PWD/flocq/Prop\""
 
+COQPROGARGS=""
+for arg in $INCLUDES; do
+  case "$arg" in
+    -I|-R|-as|compcert*)
+      COQPROGARGS="$COQPROGARGS \"$arg\"";;
+    *)
+      COQPROGARGS="$COQPROGARGS \"$PWD/$arg\"";;
+  esac
+done
 
 emacs --eval "(setq coq-prog-name \"$COQPROGNAME\")" \
  --eval "(setq coq-prog-args '($COQPROGARGS))" $1 \