From 1c55826018c5f07ee25b5771e59fe0389293cb62 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 31 Jul 2017 14:06:02 +0200 Subject: [general] Remove spurious dependency of highparsing on toplevel. `G_vernac` was depending on `toplevel` just for parsing the compat number information. IMHO this was not the right place, so I have moved the parsing bits to parsing and updated the files. This allows to finally separate the `toplevel` from Coq, which avoids linking it in alternative toplevels. --- Makefile.common | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile.common') diff --git a/Makefile.common b/Makefile.common index 85ecb1a08..2e24ac8e9 100644 --- a/Makefile.common +++ b/Makefile.common @@ -105,7 +105,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \ engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ - stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma API/API.cma + parsing/highparsing.cma stm/stm.cma toplevel/toplevel.cma API/API.cma TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma -- cgit v1.2.3