Moved JProver to a user contribution (as was decided a long time ago)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11746 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 13 deletions

diff --git a/Makefile.common b/Makefile.common
index b5c81882fd..7a40686ba3 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -298,13 +298,6 @@ EXTRACTIONCMO:=\
   contrib/extraction/extract_env.cmo \
   contrib/extraction/g_extraction.cmo
 
-JPROVERCMA:=contrib/jprover/jprover_plugin.cma
-JPROVERCMO:=\
-  contrib/jprover/opname.cmo \
-  contrib/jprover/jterm.cmo contrib/jprover/jlogic.cmo \
-  contrib/jprover/jtunify.cmo contrib/jprover/jall.cmo \
-  contrib/jprover/jprover.cmo
-
 FUNINDCMA:=contrib/funind/recdef_plugin.cma
 FUNINDCMO:=\
   contrib/funind/indfun_common.cmo contrib/funind/rawtermops.cmo \
@@ -343,13 +336,13 @@ RTAUTOCMO:=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \
 CONTRIBSTATIC:=\
 	$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
         $(QUOTECMO) $(RINGCMO) $(NEWRINGCMO) $(DPCMO) $(FIELDCMO) \
-        $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \
+        $(FOURIERCMO) $(EXTRACTIONCMO) $(XMLCMO) \
         $(CCCMO)  $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \
         $(FUNINDCMO)
 
 ifeq ($(HASNATDYNLINK),true)
  CONTRIBSTATIC:=$(SUBTACCMO)
- INITPLUGINS:=$(EXTRACTIONCMA) $(JPROVERCMA) $(FOCMA) $(CCCMA) $(DPCMA) \
+ INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \
 	$(XMLCMA) $(FUNINDCMA) #$(SUBTACCMA)
  INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
  ifeq ($(BEST),opt)
@@ -836,8 +829,6 @@ FUNINDVO:=
 RECDEFVO:=$(addprefix contrib/funind/, \
  Recdef.vo )
 
-JPROVERVO:= 
-
 CCVO:=
 
 DPVO:=$(addprefix contrib/dp/, \
@@ -847,7 +838,7 @@ RTAUTOVO:=$(addprefix contrib/rtauto/, \
  Bintree.vo	Rtauto.vo )
 
 CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
-	    $(XMLVO) $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) \
+	    $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \
 	    $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO)
 
 ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO)
@@ -915,7 +906,7 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
 VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \
   fsets allfsets relations wellfounded ints reals allreals \
   setoids sorting natural integer rational numbers noreal \
-  omega micromega ring setoid_ring dp xml extraction field fourier jprover \
+  omega micromega ring setoid_ring dp xml extraction field fourier \
   funind cc programs subtac rtauto
 DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial refman-quick refman-nodep stdlib-nodep
 STAGE3_TARGETS:=world install coqide coqide-files coq coqlib \