From b60906cc3ee3f994babf9cceff2971bd03485f2f Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Mon, 22 Jan 2018 12:45:49 -0800 Subject: Change references to CAMLP4 to CAMLP5 to be more accurate since we no longer use camlp4. --- plugins/btauto/g_btauto.ml4 | 2 -- plugins/cc/g_congruence.ml4 | 2 -- plugins/derive/g_derive.ml4 | 2 -- plugins/extraction/g_extraction.ml4 | 2 -- plugins/firstorder/g_ground.ml4 | 1 - plugins/fourier/g_fourier.ml4 | 2 -- plugins/funind/g_indfun.ml4 | 1 - plugins/ltac/coretactics.ml4 | 2 -- plugins/ltac/extraargs.ml4 | 2 -- plugins/ltac/extratactics.ml4 | 2 -- plugins/ltac/g_auto.ml4 | 2 -- plugins/ltac/g_class.ml4 | 2 -- plugins/ltac/g_eqdecide.ml4 | 2 -- plugins/ltac/g_ltac.ml4 | 4 +--- plugins/ltac/g_obligations.ml4 | 4 +--- plugins/ltac/g_rewrite.ml4 | 2 -- plugins/ltac/profile_ltac_tactics.ml4 | 2 -- plugins/micromega/g_micromega.ml4 | 2 -- plugins/nsatz/g_nsatz.ml4 | 2 -- plugins/omega/g_omega.ml4 | 2 -- plugins/quote/g_quote.ml4 | 2 -- plugins/romega/g_romega.ml4 | 2 -- plugins/rtauto/g_rtauto.ml4 | 2 -- plugins/setoid_ring/g_newring.ml4 | 2 -- plugins/ssrmatching/ssrmatching.ml4 | 3 --- 25 files changed, 2 insertions(+), 51 deletions(-) (limited to 'plugins') 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 -- cgit v1.2.3