diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-19 15:29:24 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-19 15:29:24 +0000 |
commit | bf69f9e2204de87a08ef2cc622d347b33f3f42ce (patch) | |
tree | 9d4f62320f85a700bd5079061593949f82b4ddb4 | |
parent | faa0de5c67594980f8ad871dcf71c0dc98865a5e (diff) |
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
-rw-r--r-- | doc/refman/Setoid.tex | 1 | ||||
-rw-r--r-- | plugins/funind/merge.ml | 6 | ||||
-rw-r--r-- | plugins/subtac/eterm.ml | 1 | ||||
-rw-r--r-- | plugins/subtac/subtac_cases.ml | 1 | ||||
-rw-r--r-- | plugins/subtac/subtac_classes.ml | 1 | ||||
-rw-r--r-- | plugins/subtac/subtac_coercion.ml | 1 | ||||
-rw-r--r-- | plugins/subtac/subtac_obligations.ml | 1 | ||||
-rw-r--r-- | plugins/subtac/subtac_pretyping_F.ml | 1 | ||||
-rw-r--r-- | pretyping/typeclasses.ml | 1 | ||||
-rw-r--r-- | tactics/class_tactics.ml4 | 1 | ||||
-rw-r--r-- | tactics/rewrite.ml4 | 1 | ||||
-rw-r--r-- | tools/coqdoc/cpretty.mll | 1 | ||||
-rw-r--r-- | tools/coqdoc/index.ml | 1 | ||||
-rw-r--r-- | tools/coqdoc/main.ml | 1 | ||||
-rw-r--r-- | tools/coqdoc/output.ml | 1 | ||||
-rw-r--r-- | toplevel/classes.ml | 1 |
16 files changed, 0 insertions, 21 deletions
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex index 20c8c02b7..8e1bb10c9 100644 --- a/doc/refman/Setoid.tex +++ b/doc/refman/Setoid.tex @@ -710,5 +710,4 @@ using the command \texttt{Typeclasses Opaque} (see \S \ref{TypeclassesTransparen %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" -%%% compile-command: "make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf" %%% End: diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 26f49f6d4..ccc37046f 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 bfa2d4741..9790667c4 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 4ec34a91a..29ce9d3d4 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 07b076e67..4a254d791 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 6b07e3591..1bc3dbb34 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 181d0fa72..c7d0eb67f 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 4d7bcb1eb..0dda9b9e8 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 *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index bfdc3fd8d..a460a580a 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.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/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 18d2c6081..38ae4b905 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -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/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index fd34d70f9..d2381332e 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -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/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 344d3af70..7c9533acf 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -1,4 +1,3 @@ -(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 9445c9606..1a86ce640 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -1,4 +1,3 @@ -(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index f3ebe0dc3..4fde70bf0 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -1,4 +1,3 @@ -(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 57e0afa43..392a297d6 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -1,4 +1,3 @@ -(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 40d44432e..d16147024 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.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 *) |