Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use camlp4

25 files changed, 2 insertions, 51 deletions

diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4
index 23b91507c..896bb91f1 100644
--- a/plugins/btauto/g_btauto.ml4
+++ b/plugins/btauto/g_btauto.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma"  i*)
-
 open Ltac_plugin
 
 DECLARE PLUGIN "btauto_plugin"
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 6ed4672ce..0d677ac7a 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Ltac_plugin
 open Cctac
 open Stdarg
diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4
index df701ed80..72057cd9b 100644
--- a/plugins/derive/g_derive.ml4
+++ b/plugins/derive/g_derive.ml4
@@ -8,8 +8,6 @@
 
 open Stdarg
 
-(*i camlp4deps: "grammar/grammar.cma"  i*)
-
 DECLARE PLUGIN "derive_plugin"
 
 let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 24c70bccf..4b6de58bd 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Pcoq.Prim
 
 DECLARE PLUGIN "extraction_plugin"
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index b81010c7b..3c6ab47e9 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma"  i*)
 
 open Ltac_plugin
 open Formula
diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4
index 682673e8d..16dd4c886 100644
--- a/plugins/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Ltac_plugin
 open FourierR
 
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 4b828a702..ac7a2f284 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -5,7 +5,6 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*i camlp4deps: "grammar/grammar.cma" i*)
 open Ltac_plugin
 open Util
 open Pp
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 2769802cf..7d2c4d082 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Util
 open Locus
 open Misctypes
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index bb01aca55..4c6d3c2d3 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Pp
 open Genarg
 open Stdarg
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 3e3965b94..286f9d95d 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Pp
 open Genarg
 open Stdarg
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 90a44708f..f74d24db0 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Pp
 open Genarg
 open Stdarg
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index ed2d9da63..014433ac4 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Class_tactics
 open Stdarg
 open Tacarg
diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index 549436902..f705778fc 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
@@ -12,8 +12,6 @@
 (*                           by Eduardo Gimenez                        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Eqdecide
 
 DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index cc7ce339b..9ef819569 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 DECLARE PLUGIN "ltac_plugin"
 
 open Util
@@ -17,7 +15,7 @@ open Tacexpr
 open Misctypes
 open Genarg
 open Genredexpr
-open Tok (* necessary for camlp4 *)
+open Tok (* necessary for camlp5 *)
 open Names
 
 open Pcoq
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index f6cc3833a..e251b1049 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -6,11 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 (*
   Syntax for the subtac terms and types.
-  Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *)
+  Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *)
 
 open Libnames
 open Constrexpr
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index ea1808a25..2459a09bc 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 (* Syntax for rewriting with strategies *)
 
 open Names
diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4
index 9864ffeb6..7a75662be 100644
--- a/plugins/ltac/profile_ltac_tactics.ml4
+++ b/plugins/ltac/profile_ltac_tactics.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 (** Ltac profiling entrypoints *)
 
 open Profile_ltac
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index b15dd7ae6..9f1d83f96 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -14,8 +14,6 @@
 (*                                                                      *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Ltac_plugin
 open Stdarg
 open Tacarg
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index 01c3d7940..272d4a20f 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Ltac_plugin
 
 DECLARE PLUGIN "nsatz_plugin"
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 735af6bab..f7b153a13 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -13,8 +13,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 
 DECLARE PLUGIN "omega_plugin"
 
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index f7ebd3204..40897d62f 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Ltac_plugin
 open Names
 open Misctypes
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 5fd9c9419..5b77d08de 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -6,8 +6,6 @@
 
  *************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 
 DECLARE PLUGIN "romega_plugin"
 
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index bfa1e5f39..1bfcdc2fb 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 
-(*i camlp4deps: "grammar/grammar.cma"  i*)
-
 open Ltac_plugin
 
 DECLARE PLUGIN "rtauto_plugin"
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index a7d6d5bb2..b34d12952 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Ltac_plugin
 open Pp
 open Util
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index d6dbad7a9..7d0584a00 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -12,9 +12,6 @@
  * we thus save the lexer to restore it at the end of the file *)
 let frozen_lexer = CLexer.get_keyword_state () ;;
 
-(*i camlp4use: "pa_extend.cmo" i*)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
 open Ltac_plugin
 open Names
 open Pp