From 463e46425b56360a158b44c61208060c64eb2ff5 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 29 May 2012 11:09:25 +0000 Subject: place all files specific to camlp4 syntax extensions in grammar/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15387 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/btauto/g_btauto.ml4 | 2 +- plugins/cc/cctac.ml | 2 -- plugins/cc/g_congruence.ml4 | 2 +- plugins/decl_mode/g_decl_mode.ml4 | 2 +- plugins/extraction/g_extraction.ml4 | 2 +- plugins/field/field.ml4 | 2 +- plugins/firstorder/g_ground.ml4 | 2 +- plugins/fourier/g_fourier.ml4 | 2 +- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/recdef.ml | 1 - plugins/micromega/g_micromega.ml4 | 2 +- plugins/nsatz/nsatz.ml4 | 2 +- plugins/omega/g_omega.ml4 | 2 +- plugins/quote/g_quote.ml4 | 2 +- plugins/ring/g_ring.ml4 | 2 +- plugins/romega/g_romega.ml4 | 2 +- plugins/rtauto/g_rtauto.ml4 | 2 +- plugins/setoid_ring/newring.ml4 | 2 +- plugins/xml/dumptree.ml4 | 2 +- plugins/xml/xmlentries.ml4 | 2 +- 20 files changed, 18 insertions(+), 21 deletions(-) (limited to 'plugins') diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4 index a7171b6bd..14d23a82a 100644 --- a/plugins/btauto/g_btauto.ml4 +++ b/plugins/btauto/g_btauto.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) TACTIC EXTEND btauto | [ "btauto" ] -> [ Refl_btauto.Btauto.tac ] diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 0a3697e2a..7940009c6 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) - (* This file is the interface between the c-c algorithm and Coq *) open Evd diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 881b9beeb..e4428f466 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Cctac open Tactics diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 83beece26..9a8682891 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) (* arnaud: veiller à l'aspect tutorial des commentaires *) diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 11a2d0e0d..4438c5897 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) (* ML names *) diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index 15c495ae7..988e56af5 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Names open Pp diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index a5ee551a5..b6a0ef4c3 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Formula open Sequent diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 index 9276eda1b..039d7a499 100644 --- a/plugins/fourier/g_fourier.ml4 +++ b/plugins/fourier/g_fourier.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open FourierR diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index eb90c0549..169f4d120 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Util open Term open Names diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 2005a90e3..5fcd495ef 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) open Tacexpr open Term open Namegen diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index cd87e93ec..19af8d57e 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -14,7 +14,7 @@ (* *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Quote open Ring diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index c6d23afa6..b5c8502af 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp open Errors diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 4aad8e738..0b070dbc8 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -13,7 +13,7 @@ (* *) (**************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Coq_omega open Refiner diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 4b3385677..9698ca73a 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp open Tacexpr diff --git a/plugins/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4 index e306a5319..758de80ba 100644 --- a/plugins/ring/g_ring.ml4 +++ b/plugins/ring/g_ring.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Quote open Ring diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 87e42354b..a548d4d4a 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -6,7 +6,7 @@ *************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Refl_omega open Refiner diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 index 8d103d1ba..cab5a0019 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) TACTIC EXTEND rtauto [ "rtauto" ] -> [ Refl_tauto.rtauto_tac ] diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index c2815aafa..783aebafd 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp open Errors diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4 index 8415bbd10..d0b694d97 100644 --- a/plugins/xml/dumptree.ml4 +++ b/plugins/xml/dumptree.ml4 @@ -11,7 +11,7 @@ (** Contributed by Cezary Kaliszyk, Radboud University Nijmegen *) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Tacexpr;; open Decl_mode;; open Printer;; diff --git a/plugins/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4 index d65a1bd33..597190d3e 100644 --- a/plugins/xml/xmlentries.ml4 +++ b/plugins/xml/xmlentries.ml4 @@ -12,7 +12,7 @@ (* http://helm.cs.unibo.it *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Util;; open Vernacinterp;; -- cgit v1.2.3