aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/refman/Setoid.tex1
-rw-r--r--plugins/funind/merge.ml6
-rw-r--r--plugins/subtac/eterm.ml1
-rw-r--r--plugins/subtac/subtac_cases.ml1
-rw-r--r--plugins/subtac/subtac_classes.ml1
-rw-r--r--plugins/subtac/subtac_coercion.ml1
-rw-r--r--plugins/subtac/subtac_obligations.ml1
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml1
-rw-r--r--pretyping/typeclasses.ml1
-rw-r--r--tactics/class_tactics.ml41
-rw-r--r--tactics/rewrite.ml41
-rw-r--r--tools/coqdoc/cpretty.mll1
-rw-r--r--tools/coqdoc/index.ml1
-rw-r--r--tools/coqdoc/main.ml1
-rw-r--r--tools/coqdoc/output.ml1
-rw-r--r--toplevel/classes.ml1
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 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 07:42:19 +0000