diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-08 14:26:00 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-07 02:56:18 +0200 |
| commit | 633e40b6f925556e94347c348a2804cdc1068d88 (patch) | |
| tree | b8063831a6a2ca60cf45d903dedf11f83b308fe5 /tools | |
| parent | 1d0eb5d4d6fea88abc29798ee2004b2e27e952c6 (diff) | |
[camlpX] Enrico's changes to camlp4 removal.
This removes some remaining support for camlp4 in the infrastructure
and documents the change.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 6 | ||||
| -rw-r--r-- | tools/coqmktop.ml | 13 |
2 files changed, 3 insertions, 16 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 22b1408c0..ed89bda2c 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -528,11 +528,7 @@ let variables is_install opt (args,defs) = print "CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack\n"; print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n"; print "GRAMMARS?=grammar.cma\n"; - print "ifeq ($(CAMLP4),camlp5) -CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo -else -CAMLP4EXTEND= -endif\n"; + print "CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo\n"; print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\ $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; end; diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index 645b3665e..7fa8fd58d 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -62,8 +62,6 @@ let echo = ref false let no_start = ref false let is_ocaml4 = Coq_config.caml_version.[0] <> '3' -let is_camlp5 = Coq_config.camlp4 = "camlp5" - (** {6 Includes options} *) @@ -106,7 +104,7 @@ let incl_all_subdirs dir opts = (** OCaml + CamlpX libraries *) let ocaml_libs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"] -let camlp4_libs = if is_camlp5 then ["gramlib.cma"] else ["camlp4lib.cma"] +let camlp4_libs = ["gramlib.cma"] let libobjs = ocaml_libs @ camlp4_libs (** Toplevel objects *) @@ -117,14 +115,7 @@ let ocaml_topobjs = else ["toplevellib.cma"] -let camlp4_topobjs = - if is_camlp5 then - ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"] - else - [ "Camlp4Top.cmo"; - "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo"; - "Camlp4Parsers/Camlp4OCamlParser.cmo"; - "Camlp4Parsers/Camlp4GrammarParser.cmo" ] +let camlp4_topobjs = ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"] let topobjs = ocaml_topobjs @ camlp4_topobjs |