Remove compile-command pragmas for emacs

These declarations (e.g. make -C .. bin/coqtop.byte) are quite
 annoying when debugging stuff over the whole archive: all of a
 sudden, M-x recompile isn't doing what you intended just because
 you've visited some specific files. Instead:

 - Feel free to rather add intermediate targets in the Makefile if
 they aren't there yet.

 - For avoiding typing the -C with many .. after, you can have a
 look at my recursively-descending make:
   http://www.pps.jussieu.fr/~letouzey/download/make.sh
 which is to be renamed make and placed in a bin dir with more
 priority than /usr/bin. Beware! I've already add a few bad surprises
 with this hack, but it's really convenient nonetheless.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13014 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 0 insertions, 12 deletions

diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 26f49f6d49..ccc37046f9 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -1023,9 +1023,3 @@ let relprinctype_to_funprinctype relprinctype nfuns =
     url = "citeseer.ist.psu.edu/bundy93rippling.html" }
 
  *)
-(*
-*** Local Variables: ***
-*** compile-command: "make -C ../.. plugins/funind/merge.cmo" ***
-*** indent-tabs-mode: nil ***
-*** End: ***
-*)
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index bfa2d47413..9790667c42 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -1,4 +1,3 @@
-(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
 (**
    - Get types of existentials ;
    - Flatten dependency tree (prefix order) ;
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 4ec34a91ad..29ce9d3d4a 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -1,4 +1,3 @@
-(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 07b076e673..4a254d7910 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -1,4 +1,3 @@
-(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 6b07e3591c..1bc3dbb345 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -1,4 +1,3 @@
-(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 181d0fa72d..c7d0eb67fb 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -1,4 +1,3 @@
-(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
 open Printf
 open Pp
 open Subtac_utils
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 4d7bcb1ebd..0dda9b9e88 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -1,4 +1,3 @@
-(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)