mv plugins lib/plugins

Makefile.in

@@ -208,7 +208,8 @@ clean::
 
 install_no_local::
 	mkdir -p $(BINDIR)
-	mkdir -p $(LIBDIR)/why3
+	mkdir -p $(LIBDIR)/why3/plugins
+	mkdir -p $(LIBDIR)/why3/coq
 	mkdir -p $(DATADIR)/why3/images
 	mkdir -p $(DATADIR)/why3/emacs
 	mkdir -p $(DATADIR)/why3/lang
@@ -297,7 +298,7 @@ src/realize.cmx: src/why3.cmxa
 
 clean::
 	rm -f src/realize.cm[iox] src/realize.annot src/realize.o
-	rm -f bin/realize.byte bin/realize.opt bin/realize
+	rm -f bin/why3realize.byte bin/why3realize.opt bin/why3realize
 
 install_no_local::
 	cp -f bin/why3realize.@OCAMLBEST@ $(BINDIR)/why3realize
@@ -808,22 +809,22 @@ $(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
 
 # build targets
 
-plugins.byte byte: plugins/whytptp.cmo
-plugins.opt  opt : plugins/whytptp.cmxs
+plugins.byte byte: lib/plugins/whytptp.cmo
+plugins.opt  opt : lib/plugins/whytptp.cmxs
 
-plugins/whytptp.cmxs plugins/whytptp.cmo: EXTOBJS += $(MENHIRLIB)
-plugins/whytptp.cmxs plugins/whytptp.cmo: INCLUDES += $(MENHIRINC)
+lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: EXTOBJS += $(MENHIRLIB)
+lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: INCLUDES += $(MENHIRINC)
 
-plugins/whytptp.cmxs: $(TPTPCMX)
+lib/plugins/whytptp.cmxs: $(TPTPCMX)
 	$(if $(QUIET), @echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
 
-plugins/whytptp.cmo: $(TPTPCMO)
+lib/plugins/whytptp.cmo: $(TPTPCMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^
 
 install_no_local::
-	cp -f plugins/whytptp.cm* $(LIBDIR)/why3/
+	cp -f lib/plugins/whytptp.cm* $(LIBDIR)/why3/plugins/
 
 # depend and clean targets
 
@@ -839,7 +840,7 @@ clean::
 	rm -f src/tptp2why/*.cm* src/tptp2why/*.o
 	rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
 	rm -f src/tptp2why/*.output src/tptp2why/*.automaton
-	rm -f plugins/whytptp.cm* plugins/whytptp.o
+	rm -f lib/plugins/whytptp.cm* lib/plugins/whytptp.o
 	rm -f .depend.tptp2why
 
 endif
@@ -1206,6 +1207,7 @@ DISTRIB_FILES = Version Makefile.in configure.in META.in configure .depend.* \
       examples/use_api.ml \
       theories/*.why \
       modules/*.mlw \
+      lib/coq/*/*.v \
       share/provers-detection-data.conf.in \
       share/emacs/why.el share/images/*.png share/lang/*.lang
 
@@ -1228,7 +1230,9 @@ $(DISTRIB_TAR): doc/manual.pdf
 	mkdir -p $(DISTRIB_DIR)
 	mkdir -p $(DISTRIB_DIR)/bin
 	mkdir -p $(DISTRIB_DIR)/share
-	mkdir -p $(DISTRIB_DIR)/plugins
+	mkdir -p $(DISTRIB_DIR)/lib
+	mkdir -p $(DISTRIB_DIR)/lib/plugins
+	mkdir -p $(DISTRIB_DIR)/lib/coq
 	ln -s ../drivers $(DISTRIB_DIR)/share/drivers
 	ln -s ../modules $(DISTRIB_DIR)/share/modules
 	ln -s ../theories $(DISTRIB_DIR)/share/theories

src/config.sh.in

@@ -8,7 +8,7 @@ localdir="None"
 plugins="false"
 
 if [ "@enable_local@" = "yes" ]; then
-    libdir="@LOCALDIR@/plugins"
+    libdir="@LOCALDIR@/lib"
     datadir="@LOCALDIR@/share"
     localdir="Some \"@LOCALDIR@\""
 fi

src/driver/whyconf.ml

@@ -112,7 +112,7 @@ let add_plugin m p =
   then m
   else { m with plugins = List.rev (p::(List.rev m.plugins))}
 
-let pluginsdir m = m.libdir
+let pluginsdir m = Filename.concat m.libdir "plugins"
 let load_plugins m =
   let load x =
     try Plugin.load x