diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:09:25 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:09:25 +0000 |
| commit | 463e46425b56360a158b44c61208060c64eb2ff5 (patch) | |
| tree | 7e55457a3aaa07032f8afb8528d027cac26245f4 | |
| parent | 51efb80ac1699a27e0003349bb766a430fbaf86a (diff) | |
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
45 files changed, 50 insertions, 55 deletions
diff --git a/.gitignore b/.gitignore index 8c14100cd..0cbb48297 100644 --- a/.gitignore +++ b/.gitignore @@ -111,12 +111,13 @@ g_*.ml ide/project_file.ml lib/pp.ml lib/compat.ml -parsing/q_util.ml -parsing/tacextend.ml -parsing/q_constr.ml +grammar/q_util.ml +grammar/q_constr.ml +grammar/q_coqast.ml +grammar/tacextend.ml +grammar/vernacextend.ml +grammar/argextend.ml parsing/pcoq.ml -parsing/vernacextend.ml -parsing/argextend.ml parsing/lexer.ml plugins/xml/proofTree2Xml.ml plugins/xml/acic2Xml.ml diff --git a/Makefile.build b/Makefile.build index da5e8e694..2aa4ca6d7 100644 --- a/Makefile.build +++ b/Makefile.build @@ -701,7 +701,7 @@ ml-doc: parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d $(OCAMLDOC_MLLIBD) -parsing/grammar.dot : | parsing/grammar.mllib.d +grammar/grammar.dot : | grammar/grammar.mllib.d $(OCAMLDOC_MLLIBD) tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d @@ -724,7 +724,7 @@ dev/printers.cma: | dev/printers.mllib.d $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ -parsing/grammar.cma: | parsing/grammar.mllib.d +grammar/grammar.cma: | grammar/grammar.mllib.d $(SHOW)'Testing $@' @touch test.ml4 $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) -I $(CAMLLIB) $^ -impl" -impl test.ml4 -o test-grammar diff --git a/Makefile.common b/Makefile.common index d5b152432..d7325bcbb 100644 --- a/Makefile.common +++ b/Makefile.common @@ -72,7 +72,7 @@ SRCDIRS:=\ config tools tools/coqdoc scripts lib \ kernel kernel/byterun library proofs tactics \ pretyping interp toplevel/utils toplevel parsing \ - intf ide/utils ide \ + grammar intf ide/utils ide \ $(addprefix plugins/, \ omega romega micromega quote ring \ setoid_ring xml extraction fourier \ @@ -160,7 +160,7 @@ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \ parsing/highparsing.cma tactics/hightactics.cma -GRAMMARCMA:=parsing/grammar.cma +GRAMMARCMA:=grammar/grammar.cma OMEGACMA:=plugins/omega/omega_plugin.cma ROMEGACMA:=plugins/romega/romega_plugin.cma @@ -20,7 +20,7 @@ ## tags for grammar.cm* -<parsing/grammar.{cma,cmxa}> : use_unix +<grammar/grammar.{cma,cmxa}> : use_unix ## tags for camlp4 files @@ -48,10 +48,10 @@ "plugins/decl_mode/g_decl_mode.ml4": use_compat5 "plugins/funind/g_indfun.ml4": use_compat5 -"parsing/argextend.ml4": use_compat5b -"parsing/q_constr.ml4": use_compat5b -"parsing/tacextend.ml4": use_compat5b -"parsing/vernacextend.ml4": use_compat5b +"grammar/argextend.ml4": use_compat5b +"grammar/q_constr.ml4": use_compat5b +"grammar/tacextend.ml4": use_compat5b +"grammar/vernacextend.ml4": use_compat5b <plugins/**/*.ml4>: use_grammar @@ -65,6 +65,7 @@ "ide/utils": include "interp": include "intf": include +"grammar": include "kernel": include "kernel/byterun": include "lib": include diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 80da0c8b0..b63f3ee26 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -2013,7 +2013,7 @@ containing: \begin{itemize} \item in \verb+g_hello.ml4+: \begin{verbatim} -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) TACTIC EXTEND Hello | [ "hello" ] -> [ Coq_hello.printHello ] END diff --git a/parsing/argextend.ml4 b/grammar/argextend.ml4 index 5a64580d2..a13059799 100644 --- a/parsing/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -337,4 +337,3 @@ EXTEND ] ] ; END - diff --git a/parsing/grammar.mllib b/grammar/grammar.mllib index 313676c96..195ad38c0 100644 --- a/parsing/grammar.mllib +++ b/grammar/grammar.mllib @@ -23,7 +23,6 @@ Extrawit Pcoq Q_util Q_coqast - Egramml Argextend Tacextend diff --git a/parsing/q_constr.ml4 b/grammar/q_constr.ml4 index d78b6c8c0..fe4ccc53d 100644 --- a/parsing/q_constr.ml4 +++ b/grammar/q_constr.ml4 @@ -124,4 +124,3 @@ EXTEND open Coqlib let a = PATTERN [ match ?X with %path_of_S n => n | %path_of_O => ?X end ] *) - diff --git a/parsing/q_coqast.ml4 b/grammar/q_coqast.ml4 index 7467a32f0..7467a32f0 100644 --- a/parsing/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 diff --git a/parsing/q_util.ml4 b/grammar/q_util.ml4 index cfaa2a654..cfaa2a654 100644 --- a/parsing/q_util.ml4 +++ b/grammar/q_util.ml4 diff --git a/parsing/q_util.mli b/grammar/q_util.mli index 5d56c456f..5d56c456f 100644 --- a/parsing/q_util.mli +++ b/grammar/q_util.mli diff --git a/parsing/tacextend.ml4 b/grammar/tacextend.ml4 index ec0784c52..3a47ade0d 100644 --- a/parsing/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -232,4 +232,3 @@ EXTEND ] ] ; END - diff --git a/parsing/vernacextend.ml4 b/grammar/vernacextend.ml4 index 94135d121..af7ee7d16 100644 --- a/parsing/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -46,7 +46,7 @@ let make_fun_clauses loc s l = let mlexpr_of_clause = mlexpr_of_list - (fun (a,b,c) -> mlexpr_of_list make_prod_item + (fun (a,b,c) -> mlexpr_of_list make_prod_item (Option.List.cons (Option.map (fun a -> GramTerminal a) a) b)) let declare_command loc s nt cl = @@ -68,7 +68,7 @@ EXTEND [ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT; OPT "|"; l = LIST1 rule SEP "|"; "END" -> - declare_command loc s <:expr<None>> l + declare_command loc s <:expr<None>> l | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; OPT "|"; l = LIST1 rule SEP "|"; "END" -> diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 7700d9959..966eb6c1c 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -278,8 +278,8 @@ let extra_rules () = begin T(tags_of_pathname ml4 ++ "p4option"); camlp4compat; A"-o"; Px ml; A"-impl"; P ml4])); - flag_and_dep ["p4mod"; "use_grammar"] (P "parsing/grammar.cma"); - flag_and_dep ["p4mod"; "use_constr"] (P "parsing/q_constr.cmo"); + flag_and_dep ["p4mod"; "use_grammar"] (P "grammar/grammar.cma"); + flag_and_dep ["p4mod"; "use_constr"] (P "grammar/q_constr.cmo"); flag_and_dep ["p4mod"; "use_compat5"] (P "tools/compat5.cmo"); flag_and_dep ["p4mod"; "use_compat5b"] (P "tools/compat5b.cmo"); diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4 index d763a1cab..d4229ff0b 100644 --- a/parsing/g_obligations.ml4 +++ b/parsing/g_obligations.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*) (* Syntax for the subtac terms and types. diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib index 6ccbdb752..13ed80464 100644 --- a/parsing/highparsing.mllib +++ b/parsing/highparsing.mllib @@ -4,4 +4,4 @@ G_prim G_proofs G_tactic G_ltac -G_obligations
\ No newline at end of file +G_obligations 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;; diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index a749ba8ab..d62320e76 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.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/tactics/eauto.ml4 b/tactics/eauto.ml4 index fb692873e..1cde368a1 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.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/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 1a65f6278..6a8884355 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -12,7 +12,7 @@ (* by Eduardo Gimenez *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Errors open Util diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 4677d87ef..bff4f4760 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.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 Pcoq diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index db55f6434..82b08289d 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.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 Pcoq diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 5abbe7ae9..bc9121911 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*) +(*i camlp4deps: "grammar/grammar.cma grammar/q_constr.cmo" i*) open Pp open Errors diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 004599f45..16eb595ea 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.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/tactics/tauto.ml4 b/tactics/tauto.ml4 index 79c1797e4..0ab78fcd6 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.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 Term open Hipattern diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index d869e8854..71c17b9ac 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.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 Flags open Pp |