diff options
Diffstat (limited to 'plugins')
| -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 |
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 *) |