Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

1 files changed, 17 insertions, 26 deletions

diff --git a/Makefile.common b/Makefile.common
index 509ceedb..0a5d4260 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -46,8 +46,6 @@ COQBINARIES:= $(COQMKTOP) $(COQC) \
 endif
 OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE)
 
-MINICOQ:=bin/minicoq$(EXE)
-
 CSDPCERT:=bin/csdpcert$(EXE)
 
 ###########################################################################
@@ -88,7 +86,7 @@ REFMANCOQTEXFILES:=\
   doc/refman/RefMan-oth.v.tex doc/refman/RefMan-ltac.v.tex \
   doc/refman/RefMan-decl.v.tex \
   doc/refman/Cases.v.tex doc/refman/Coercion.v.tex doc/refman/Extraction.v.tex \
-  doc/refman/Program.v.tex doc/refman/Omega.v.tex doc/refman/Polynom.v.tex \
+  doc/refman/Program.v.tex doc/refman/Omega.v.tex doc/refman/Micromega.v.tex doc/refman/Polynom.v.tex \
   doc/refman/Setoid.v.tex doc/refman/Helm.tex doc/refman/Classes.v.tex
 
 REFMANTEXFILES:=\
@@ -123,8 +121,8 @@ CONFIG:=\
   config/coq_config.cmo
 
 LIBREP:=\
-  lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/util.cmo lib/bigint.cmo \
-  lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/flags.cmo \
+  lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \
+  lib/util.cmo lib/bigint.cmo lib/hashcons.cmo lib/dyn.cmo lib/system.cmo \
   lib/bstack.cmo lib/edit.cmo lib/gset.cmo lib/gmap.cmo \
   lib/tlm.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo \
   lib/predicate.cmo lib/rtree.cmo lib/heap.cmo lib/option.cmo
@@ -411,8 +409,8 @@ COQDOCCMO:=$(CONFIG) tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmo \
 MCHECKER:=\
   config/coq_config.cmo \
   lib/pp_control.cmo lib/pp.cmo lib/compat.cmo \
-  lib/util.cmo lib/option.cmo lib/hashcons.cmo \
-  lib/system.cmo lib/flags.cmo \
+  lib/flags.cmo lib/util.cmo lib/option.cmo lib/hashcons.cmo \
+  lib/system.cmo \
   lib/predicate.cmo lib/rtree.cmo \
   kernel/names.cmo kernel/univ.cmo \
   kernel/esubst.cmo checker/term.cmo \
@@ -426,17 +424,11 @@ MCHECKER:=\
   checker/safe_typing.cmo checker/check.cmo \
   checker/check_stat.cmo checker/checker.cmo
 
-# minicoq
-
-MINICOQCMO:=$(CONFIG) $(LIBREP) $(KERNEL) \
-	   parsing/lexer.cmo parsing/g_minicoq.cmo \
-	   toplevel/fhimsg.cmo toplevel/minicoq.cmo
-
 # grammar modules with camlp4
 
 GRAMMARNEEDEDCMO:=\
-  lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/util.cmo lib/bigint.cmo \
-  lib/dyn.cmo lib/flags.cmo lib/hashcons.cmo lib/predicate.cmo \
+  lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \
+  lib/util.cmo lib/bigint.cmo lib/dyn.cmo lib/hashcons.cmo lib/predicate.cmo \
   lib/rtree.cmo lib/option.cmo \
   kernel/names.cmo kernel/univ.cmo \
   kernel/esubst.cmo kernel/term.cmo kernel/mod_subst.cmo kernel/sign.cmo \
@@ -469,7 +461,7 @@ GRAMMARSCMO:=\
   parsing/g_prim.cmo parsing/g_tactic.cmo \
   parsing/g_ltac.cmo parsing/g_constr.cmo
 
-GRAMMARCMO:=$(GRAMMARNEEDEDCMO) $(CAMLP4EXTENSIONSCMO) $(GRAMMARSCMO)
+GRAMMARCMO:=$(CONFIG) $(GRAMMARNEEDEDCMO) $(CAMLP4EXTENSIONSCMO) $(GRAMMARSCMO)
 
 GRAMMARCMA:=parsing/grammar.cma
 
@@ -511,9 +503,9 @@ PRINTERSCMO:=\
   parsing/lexer.cmo interp/ppextend.cmo interp/genarg.cmo \
   interp/topconstr.cmo interp/notation.cmo interp/reserve.cmo		\
   library/impargs.cmo interp/constrextern.cmo \
-  interp/syntax_def.cmo interp/implicit_quantifiers.cmo  interp/constrintern.cmo \
-  proofs/proof_trees.cmo proofs/logic.cmo proofs/refiner.cmo \
-  proofs/tacexpr.cmo \
+  interp/syntax_def.cmo interp/implicit_quantifiers.cmo \
+  interp/constrintern.cmo proofs/proof_trees.cmo proofs/tacexpr.cmo \
+  proofs/proof_type.cmo proofs/logic.cmo proofs/refiner.cmo \
   proofs/evar_refiner.cmo proofs/pfedit.cmo proofs/tactic_debug.cmo \
   proofs/decl_mode.cmo \
   parsing/ppconstr.cmo parsing/extend.cmo parsing/pcoq.cmo \
@@ -622,8 +614,8 @@ FSETSVO:=$(FSETSBASEVO) $(FSETS_$(FSETS))
 ALLFSETS:=$(FSETSBASEVO) $(FSETS_all)
 
 RELATIONSVO:=$(addprefix theories/Relations/, \
- Newman.vo 		Operators_Properties.vo	Relation_Definitions.vo \
- Relation_Operators.vo 	Relations.vo 		Rstar.vo )
+ Operators_Properties.vo	Relation_Definitions.vo \
+ Relation_Operators.vo 		Relations.vo )
 
 WELLFOUNDEDVO:=$(addprefix theories/Wellfounded/, \
  Disjoint_Union.vo 	Inclusion.vo 	Inverse_Image.vo \
@@ -723,8 +715,7 @@ RATIONALSPECVIAQVO:=$(addprefix theories/Numbers/Rational/SpecViaQ/, \
  QSig.vo )
 
 RATIONALBIGQVO:=$(addprefix theories/Numbers/Rational/BigQ/, \
- QMake_base.vo	QpMake.vo	QvMake.vo	Q0Make.vo 	\
- QifMake.vo 	QbiMake.vo 	BigQ.vo )
+ QMake.vo	BigQ.vo )
 
 RATIONALVO:=$(RATIONALSPECVIAQVO) $(RATIONALBIGQVO)
 
@@ -767,7 +758,7 @@ MICROMEGAVO:=$(addprefix contrib/micromega/, \
   Env.vo                RingMicromega.vo \
   EnvRing.vo            VarMap.vo \
   OrderedRing.vo        ZCoeff.vo \
-  Micromegatac.vo       ZMicromega.vo \
+  Psatz.vo	       ZMicromega.vo \
   QMicromega.vo         RMicromega.vo \
   Tauto.vo )
 
@@ -872,13 +863,13 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
   interp parsing pretyping highparsing toplevel hightactics \
   coqide-binaries coqide-byte coqide-opt $(COQIDEOPT) $(COQIDEBYTE) $(COQIDE) \
   pcoq-binaries $(COQINTERFACE) $(CSDPCERT) coqbinaries pcoq $(TOOLS) tools \
-  printers $(MINICOQ) debug
+  printers debug
 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 \
   funind cc programs subtac rtauto
-DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial
+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 \
   coqlight states pcoq-files check init theories theories-light contrib \
   $(DOC_TARGETS) $(VO_TARGETS)