Imported Upstream version 8.6upstream/8.6

1 files changed, 90 insertions, 302 deletions

diff --git a/Makefile.common b/Makefile.common
index 1a903539..49fe1fd9 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -14,19 +14,32 @@
 
 COQMKTOP:=bin/coqmktop$(EXE) 
 
-COQC:=bin/coqc$(EXE)
-
 COQTOPBYTE:=bin/coqtop.byte$(EXE)
 COQTOPEXE:=bin/coqtop$(EXE)
 
-CHICKENBYTE:=bin/coqchk.byte$(EXE)
-CHICKEN:=bin/coqchk$(EXE)
+COQDEP:=bin/coqdep$(EXE)
+COQMAKEFILE:=bin/coq_makefile$(EXE)
+GALLINA:=bin/gallina$(EXE)
+COQTEX:=bin/coq-tex$(EXE)
+COQWC:=bin/coqwc$(EXE)
+COQDOC:=bin/coqdoc$(EXE)
+COQC:=bin/coqc$(EXE)
+COQWORKMGR:=bin/coqworkmgr$(EXE)
 
-ifeq ($(CAMLP4),camlp4)
-CAMLP4MOD:=camlp4lib
-else
-CAMLP4MOD:=gramlib
-endif
+TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
+	$(COQWORKMGR)
+
+COQDEPBOOT:=bin/coqdep_boot$(EXE)
+OCAMLLIBDEP:=bin/ocamllibdep$(EXE)
+FAKEIDE:=bin/fake_ide$(EXE)
+
+PRIVATEBINARIES:=$(FAKEIDE) $(OCAMLLIBDEP) $(COQDEPBOOT)
+
+CSDPCERT:=plugins/micromega/csdpcert$(EXE)
+
+###########################################################################
+# Object and Source files
+###########################################################################
 
 ifeq ($(HASNATDYNLINK)-$(BEST),true-opt)
   DEPNATDYN:=
@@ -39,119 +52,22 @@ INSTALLLIB:=install -m 644
 INSTALLSH:=./install.sh
 MKDIR:=install -d
 
-COQIDEBYTE:=bin/coqide.byte$(EXE)
-COQIDE:=bin/coqide$(EXE)
-COQIDEAPP:=bin/CoqIDE_$(VERSION).app
-COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide
-
-ifeq ($(BEST),opt)
-OPT:=opt
-else
-OPT:=
-endif
-
-BESTOBJ:=$(if $(OPT),.cmx,.cmo)
-BESTLIB:=$(if $(OPT),.cmxa,.cma)
-BESTDYN:=$(if $(OPT),.cmxs,.cma)
-
-COQBINARIES:= $(COQMKTOP) \
-  $(COQTOPBYTE) $(COQTOPEXE) \
-  $(CHICKENBYTE) $(CHICKEN)
-
-CSDPCERT:=plugins/micromega/csdpcert$(EXE)
-
 CORESRCDIRS:=\
   config 	lib		kernel		kernel/byterun	library \
   proofs 	tactics 	pretyping	interp		stm \
-  toplevel	parsing	printing	grammar	        intf
+  toplevel	parsing 	printing	intf	engine	ltac
 
-PLUGINS:=\
+PLUGINDIRS:=\
   omega		romega 		micromega 	quote \
   setoid_ring 	extraction 	fourier \
   cc 		funind 		firstorder 	derive \
-  rtauto 	nsatz           syntax          decl_mode	btauto
+  rtauto 	nsatz           syntax          decl_mode	btauto \
+  ssrmatching
 
 SRCDIRS:=\
   $(CORESRCDIRS)  \
   tools 	tools/coqdoc	\
-  $(addprefix plugins/, $(PLUGINS))
-
-IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils
-
-# Order is relevant here because kernel and checker contain files
-# with the same name
-CHKSRCDIRS:= checker lib config kernel parsing
-
-###########################################################################
-# Tools
-###########################################################################
-
-COQDEP:=bin/coqdep$(EXE)
-COQDEPBOOT:=bin/coqdep_boot$(EXE)
-COQMAKEFILE:=bin/coq_makefile$(EXE)
-GALLINA:=bin/gallina$(EXE)
-COQTEX:=bin/coq-tex$(EXE)
-COQWC:=bin/coqwc$(EXE)
-COQDOC:=bin/coqdoc$(EXE)
-FAKEIDE:=bin/fake_ide$(EXE)
-COQWORKMGR:=bin/coqworkmgr$(EXE)
-
-TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
-	$(COQWORKMGR)
-
-PRIVATEBINARIES:=$(FAKEIDE) $(COQDEPBOOT)
-
-###########################################################################
-# Documentation
-###########################################################################
-
-LATEX:=latex
-BIBTEX:=BIBINPUTS=.: bibtex -min-crossrefs=10
-MAKEINDEX:=makeindex
-PDFLATEX:=pdflatex
-DVIPS:=dvips
-FIG2DEV:=fig2dev
-CONVERT:=convert
-HEVEA:=hevea
-HACHA:=hacha
-HEVEAOPTS:=-fix -exec xxdate.exe
-HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea
-HTMLSTYLE:=simple
-export TEXINPUTS:=$(HEVEALIB):
-COQTEXOPTS:=-boot -n 72 -sl -small
-
-DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex 
-
-REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
-  RefMan-gal.v.tex RefMan-ext.v.tex \
-  RefMan-mod.v.tex RefMan-tac.v.tex \
-  RefMan-cic.v.tex RefMan-lib.v.tex \
-  RefMan-tacex.v.tex RefMan-syn.v.tex \
-  RefMan-oth.v.tex RefMan-ltac.v.tex \
-  RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \
-  Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
-  Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
-  Setoid.v.tex Classes.v.tex Universes.v.tex \
-  Misc.v.tex)
-
-REFMANTEXFILES:=$(addprefix doc/refman/, \
-  headers.sty Reference-Manual.tex \
-  RefMan-pre.tex RefMan-int.tex RefMan-com.tex \
-  RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex \
-  AsyncProofs.tex ) \
-  $(REFMANCOQTEXFILES) \
-
-REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps
-
-REFMANFILES:=$(REFMANTEXFILES) $(DOCCOMMON) $(REFMANEPSFILES) doc/refman/biblio.bib
-
-REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png)
-
-
-
-###########################################################################
-# Object and Source files 
-###########################################################################
+  $(addprefix plugins/, $(PLUGINDIRS))
 
 COQRUN := coqrun
 LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a
@@ -161,111 +77,69 @@ BYTERUN:=$(addprefix kernel/byterun/, \
   coq_fix_code.o coq_memory.o coq_values.o coq_interp.o )
 
 # LINK ORDER:
-# Beware that highparsing.cma should appear before hightactics.cma
+# Beware that highparsing.cma should appear before ltac.cma
 # respecting this order is useful for developers that want to load or link
 # the libraries directly
 
 CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
-        pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
+        engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
         parsing/parsing.cma printing/printing.cma tactics/tactics.cma \
-	stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma
+	stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma ltac/ltac.cma
 
 TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
 
-GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma
-
-OMEGACMA:=plugins/omega/omega_plugin.cma
-ROMEGACMA:=plugins/romega/romega_plugin.cma
-MICROMEGACMA:=plugins/micromega/micromega_plugin.cma
-QUOTECMA:=plugins/quote/quote_plugin.cma
-RINGCMA:=plugins/setoid_ring/newring_plugin.cma
-NSATZCMA:=plugins/nsatz/nsatz_plugin.cma
-FOURIERCMA:=plugins/fourier/fourier_plugin.cma
-EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cma
-FUNINDCMA:=plugins/funind/recdef_plugin.cma
-FOCMA:=plugins/firstorder/ground_plugin.cma
-CCCMA:=plugins/cc/cc_plugin.cma
-BTAUTOCMA:=plugins/btauto/btauto_plugin.cma
-RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cma
-NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cma
-OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \
-        z_syntax_plugin.cma \
-        numbers_syntax_plugin.cma \
-        r_syntax_plugin.cma \
-	ascii_syntax_plugin.cma \
-        string_syntax_plugin.cma )
-DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma
-DERIVECMA:=plugins/derive/derive_plugin.cma
-
-PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \
-        $(QUOTECMA) $(RINGCMA) \
-        $(FOURIERCMA) $(EXTRACTIONCMA) \
-        $(CCCMA)  $(FOCMA) $(RTAUTOCMA) $(BTAUTOCMA) \
-        $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) \
-	$(DERIVECMA)
-
-ifneq ($(HASNATDYNLINK),false)
- STATICPLUGINS:=
- INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \
-	$(FUNINDCMA) $(NATSYNTAXCMA)
- INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
- PLUGINS:=$(PLUGINSCMA)
- PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs)
-else
-ifeq ($(BEST),byte)
- STATICPLUGINS:=
- INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \
-	$(FUNINDCMA) $(NATSYNTAXCMA)
- INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
- PLUGINS:=$(PLUGINSCMA)
- PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs)
-else
- STATICPLUGINS:=$(PLUGINSCMA)
- INITPLUGINS:=
- INITPLUGINSOPT:=
- PLUGINS:=
- PLUGINSOPT:=
-endif
-endif
-
-LINKCMO:=$(CORECMA) $(STATICPLUGINS)
-LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
-
-IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo lib/errors.cmo lib/spawn.cmo
-IDECMA:=ide/ide.cma
-IDETOPLOOPCMA=ide/coqidetop.cma
-
-LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.ml
-LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml
+GRAMMARCMA:=grammar/compat5.cmo grammar/grammar.cma
 
 # modules known by the toplevel of Coq
 
 OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib))
 
-IDEMOD:=$(shell cat ide/ide.mllib)
-
-# coqmktop, coqc
-
-COQENVCMO:=lib/clib.cma lib/errors.cmo
-
-COQMKTOPCMO:=$(COQENVCMO) tools/tolink.cmo tools/coqmktop.cmo
-
-COQCCMO:=$(COQENVCMO) toplevel/usage.cmo tools/coqc.cmo
-
-## Misc
-
-CSDPCERTCMO:=$(addprefix plugins/micromega/, \
-  mutils.cmo 	micromega.cmo \
-  sos_types.cmo sos_lib.cmo sos.cmo 	csdpcert.cmo )
-
-DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma
-
-COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo
-
-COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \
-  cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo )
+###########################################################################
+# plugins object files
+###########################################################################
+
+OMEGACMO:=plugins/omega/omega_plugin.cmo
+ROMEGACMO:=plugins/romega/romega_plugin.cmo
+MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo
+QUOTECMO:=plugins/quote/quote_plugin.cmo
+RINGCMO:=plugins/setoid_ring/newring_plugin.cmo
+NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo
+FOURIERCMO:=plugins/fourier/fourier_plugin.cmo
+EXTRACTIONCMO:=plugins/extraction/extraction_plugin.cmo
+FUNINDCMO:=plugins/funind/recdef_plugin.cmo
+FOCMO:=plugins/firstorder/ground_plugin.cmo
+CCCMO:=plugins/cc/cc_plugin.cmo
+BTAUTOCMO:=plugins/btauto/btauto_plugin.cmo
+RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo
+NATSYNTAXCMO:=plugins/syntax/nat_syntax_plugin.cmo
+OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \
+        z_syntax_plugin.cmo \
+        numbers_syntax_plugin.cmo \
+        r_syntax_plugin.cmo \
+	ascii_syntax_plugin.cmo \
+        string_syntax_plugin.cmo )
+DECLMODECMO:=plugins/decl_mode/decl_mode_plugin.cmo
+DERIVECMO:=plugins/derive/derive_plugin.cmo
+SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
+
+PLUGINSCMO:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \
+        $(QUOTECMO) $(RINGCMO) \
+        $(FOURIERCMO) $(EXTRACTIONCMO) \
+        $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
+        $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \
+	$(DERIVECMO) $(SSRMATCHINGCMO)
+
+ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
+ STATICPLUGINS:=$(PLUGINSCMO)
+ PLUGINS:=
+else
+ STATICPLUGINS:=
+ PLUGINS:=$(PLUGINSCMO)
+endif
+PLUGINSOPT:=$(PLUGINSCMO:.cmo=.cmxs)
 
-COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo
+LINKCMO:=$(CORECMA) $(STATICPLUGINS)
+LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx)
 
 ###########################################################################
 # vo files
@@ -273,127 +147,41 @@ COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo
 
 ## we now retrieve the names of .vo file to compile in */vo.itarget files
 
-cat_vo_itarget = $(addprefix $(1)/,$(shell cat $(1)/vo.itarget))
-
-## Theories
-
-INITVO:=$(call cat_vo_itarget, theories/Init)
-LOGICVO:=$(call cat_vo_itarget, theories/Logic)
-STRUCTURESVO:=$(call cat_vo_itarget, theories/Structures)
-ARITHVO:=$(call cat_vo_itarget, theories/Arith)
-SORTINGVO:=$(call cat_vo_itarget, theories/Sorting)
-BOOLVO:=$(call cat_vo_itarget, theories/Bool)
-PARITHVO:=$(call cat_vo_itarget, theories/PArith)
-NARITHVO:=$(call cat_vo_itarget, theories/NArith)
-ZARITHVO:=$(call cat_vo_itarget, theories/ZArith)
-QARITHVO:=$(call cat_vo_itarget, theories/QArith)
-LISTSVO:=$(call cat_vo_itarget, theories/Lists)
-VECTORSVO:=$(call cat_vo_itarget, theories/Vectors)
-STRINGSVO:=$(call cat_vo_itarget, theories/Strings)
-SETSVO:=$(call cat_vo_itarget, theories/Sets)
-FSETSVO:=$(call cat_vo_itarget, theories/FSets)
-MSETSVO:=$(call cat_vo_itarget, theories/MSets)
-RELATIONSVO:=$(call cat_vo_itarget, theories/Relations)
-WELLFOUNDEDVO:=$(call cat_vo_itarget, theories/Wellfounded)
-REALSVO:=$(call cat_vo_itarget, theories/Reals)
-NUMBERSVO:=$(call cat_vo_itarget, theories/Numbers)
-SETOIDSVO:=$(call cat_vo_itarget, theories/Setoids)
-UNICODEVO:=$(call cat_vo_itarget, theories/Unicode)
-CLASSESVO:=$(call cat_vo_itarget, theories/Classes)
-PROGRAMVO:=$(call cat_vo_itarget, theories/Program)
-COMPATVO:=$(call cat_vo_itarget, theories/Compat)
-
-THEORIESVO:=\
-  $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) \
-  $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) \
-  $(RELATIONSVO) $(WELLFOUNDEDVO) $(SETOIDSVO) \
-  $(LISTSVO) $(STRINGSVO) \
-  $(PARITHVO) $(NARITHVO) $(ZARITHVO) \
-  $(SETSVO) $(FSETSVO) $(MSETSVO) \
-  $(REALSVO)  $(SORTINGVO) $(QARITHVO) \
-  $(NUMBERSVO) $(STRUCTURESVO) $(VECTORSVO) \
-  $(COMPATVO)
-
-THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(UNICODEVO) $(ARITHVO)
-
-## Plugins
-
-OMEGAVO:=$(call cat_vo_itarget, plugins/omega)
-ROMEGAVO:=$(call cat_vo_itarget, plugins/romega)
-MICROMEGAVO:=$(call cat_vo_itarget, plugins/micromega)
-QUOTEVO:=$(call cat_vo_itarget, plugins/quote)
-RINGVO:=$(call cat_vo_itarget, plugins/setoid_ring)
-NSATZVO:=$(call cat_vo_itarget, plugins/nsatz)
-FOURIERVO:=$(call cat_vo_itarget, plugins/fourier)
-FUNINDVO:=$(call cat_vo_itarget, plugins/funind)
-BTAUTOVO:=$(call cat_vo_itarget, plugins/btauto)
-RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto)
-EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction)
-CCVO:=
-DERIVEVO:=$(call cat_vo_itarget, plugins/derive)
-
-PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) \
-	    $(FOURIERVO) $(CCVO) $(FUNINDVO) \
-	    $(RTAUTOVO) $(BTAUTOVO) $(RINGVO) $(QUOTEVO) \
-            $(NSATZVO) $(EXTRACTIONVO) $(DERIVEVO)
+THEORIESVO:= $(foreach f, $(wildcard theories/*/vo.itarget), \
+                $(addprefix $(dir $(f)),$(shell cat $(f))))
+
+PLUGINSVO:=  $(foreach f, $(wildcard plugins/*/vo.itarget), \
+                $(addprefix $(dir $(f)),$(shell cat $(f))))
 
 ALLVO:= $(THEORIESVO) $(PLUGINSVO)
 VFILES:= $(ALLVO:.vo=.v)
+
+## More specific targets
+
+THEORIESLIGHTVO:= \
+ $(filter theories/Init/% theories/Logic/% theories/Unicode/% theories/Arith/%, $(THEORIESVO))
+
 ALLSTDLIB := test-suite/misc/universes/all_stdlib
 
 # convert a (stdlib) filename into a module name:
 # remove .vo, replace theories and plugins by Coq, and replace slashes by dots
 vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))
 
+ALLMODS:=$(call vo_to_mod,$(ALLVO))
+
+
 # Converting a stdlib filename into native compiler filenames
 # Used for install targets
 vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*)))))
 
 vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o)))))
 
-ALLMODS:=$(call vo_to_mod,$(ALLVO))
-
 LIBFILES:=$(THEORIESVO) $(PLUGINSVO) $(call vo_to_cm,$(THEORIESVO)) \
 	    $(call vo_to_cm,$(PLUGINSVO)) $(call vo_to_obj,$(THEORIESVO)) \
 	    $(call vo_to_obj,$(PLUGINSVO)) \
 	    $(PLUGINSVO:.vo=.v) $(THEORIESVO:.vo=.v) \
 	    $(PLUGINSVO:.vo=.glob) $(THEORIESVO:.vo=.glob)
 
-LIBFILESLIGHT:=$(THEORIESLIGHTVO)
-
-###########################################################################
-# Miscellaneous
-###########################################################################
-
-MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
-	man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \
-	man/coqwc.1 man/coqdoc.1 man/coqide.1 \
-	man/coq_makefile.1 man/coqmktop.1 man/coqchk.1
-
-###########################################################################
-# Source documentation
-###########################################################################
-
-OCAMLDOCDIR=dev/ocamldoc
-
-DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \
-	./pretyping/*.mli ./interp/*.mli printing/*.mli \
-	./parsing/*.mli ./proofs/*.mli \
-	./tactics/*.mli ./stm/*.mli ./toplevel/*.mli)
-
-# Defining options to generate dependencies graphs
-DOT=dot
-ODOCDOTOPTS=-dot -dot-reduce
-
-###########################################################################
-# GTK for Coqide MacOS bundle
-###########################################################################
-
-GTKSHARE=$(shell pkg-config --variable=prefix gtk+-2.0)/share
-GTKBIN=$(shell pkg-config --variable=prefix gtk+-2.0)/bin
-GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0)
-
-
 # For emacs: 
 # Local Variables: 
 # mode: makefile