Option pour compiler une version 'light' des réels

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

5 files changed, 144 insertions, 92 deletions

diff --git a/.depend b/.depend
index 927d79786..6644799b4 100644
--- a/.depend
+++ b/.depend
@@ -940,24 +940,24 @@ parsing/pptactic.cmx: kernel/closure.cmx lib/dyn.cmx parsing/egrammar.cmx \
     library/nameops.cmx kernel/names.cmx lib/pp.cmx parsing/ppconstr.cmx \
     parsing/printer.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx \
     kernel/term.cmx interp/topconstr.cmx lib/util.cmx parsing/pptactic.cmi 
-parsing/prettyp.cmo: pretyping/classops.cmi kernel/declarations.cmi \
-    library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \
-    library/global.cmi library/impargs.cmi kernel/inductive.cmi \
-    pretyping/inductiveops.cmi pretyping/instantiate.cmi library/lib.cmi \
-    library/libnames.cmi library/libobject.cmi library/nameops.cmi \
-    kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \
-    parsing/printmod.cmi kernel/reduction.cmi kernel/safe_typing.cmi \
-    kernel/sign.cmi interp/syntax_def.cmi kernel/term.cmi \
-    pretyping/termops.cmi lib/util.cmi parsing/prettyp.cmi 
-parsing/prettyp.cmx: pretyping/classops.cmx kernel/declarations.cmx \
-    library/declare.cmx kernel/environ.cmx pretyping/evd.cmx \
-    library/global.cmx library/impargs.cmx kernel/inductive.cmx \
-    pretyping/inductiveops.cmx pretyping/instantiate.cmx library/lib.cmx \
-    library/libnames.cmx library/libobject.cmx library/nameops.cmx \
-    kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \
-    parsing/printmod.cmx kernel/reduction.cmx kernel/safe_typing.cmx \
-    kernel/sign.cmx interp/syntax_def.cmx kernel/term.cmx \
-    pretyping/termops.cmx lib/util.cmx parsing/prettyp.cmi 
+parsing/prettyp.cmo: pretyping/classops.cmi interp/constrextern.cmi \
+    kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
+    pretyping/evd.cmi library/global.cmi library/impargs.cmi \
+    kernel/inductive.cmi pretyping/inductiveops.cmi pretyping/instantiate.cmi \
+    library/lib.cmi library/libnames.cmi library/libobject.cmi \
+    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
+    parsing/printer.cmi parsing/printmod.cmi kernel/reduction.cmi \
+    kernel/safe_typing.cmi kernel/sign.cmi interp/syntax_def.cmi \
+    kernel/term.cmi pretyping/termops.cmi lib/util.cmi parsing/prettyp.cmi 
+parsing/prettyp.cmx: pretyping/classops.cmx interp/constrextern.cmx \
+    kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \
+    pretyping/evd.cmx library/global.cmx library/impargs.cmx \
+    kernel/inductive.cmx pretyping/inductiveops.cmx pretyping/instantiate.cmx \
+    library/lib.cmx library/libnames.cmx library/libobject.cmx \
+    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
+    parsing/printer.cmx parsing/printmod.cmx kernel/reduction.cmx \
+    kernel/safe_typing.cmx kernel/sign.cmx interp/syntax_def.cmx \
+    kernel/term.cmx pretyping/termops.cmx lib/util.cmx parsing/prettyp.cmi 
 parsing/printer.cmo: parsing/ast.cmi interp/constrextern.cmi \
     parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \
     parsing/extend.cmi library/global.cmi library/libnames.cmi \
@@ -2326,24 +2326,22 @@ contrib/extraction/extract_env.cmx: contrib/extraction/common.cmx \
     library/nametab.cmx lib/pp.cmx contrib/extraction/table.cmx \
     kernel/term.cmx lib/util.cmx toplevel/vernacinterp.cmx \
     contrib/extraction/extract_env.cmi 
-contrib/extraction/extraction.cmo: kernel/closure.cmi kernel/declarations.cmi \
-    kernel/environ.cmi pretyping/evd.cmi library/global.cmi lib/gmap.cmi \
-    lib/gset.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \
-    pretyping/instantiate.cmi library/libnames.cmi \
+contrib/extraction/extraction.cmo: kernel/declarations.cmi kernel/environ.cmi \
+    pretyping/evd.cmi library/global.cmi lib/gmap.cmi lib/gset.cmi \
+    kernel/inductive.cmi pretyping/inductiveops.cmi library/libnames.cmi \
     contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
     library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
-    pretyping/reductionops.cmi pretyping/retyping.cmi library/summary.cmi \
-    contrib/extraction/table.cmi kernel/term.cmi pretyping/termops.cmi \
-    lib/util.cmi contrib/extraction/extraction.cmi 
-contrib/extraction/extraction.cmx: kernel/closure.cmx kernel/declarations.cmx \
-    kernel/environ.cmx pretyping/evd.cmx library/global.cmx lib/gmap.cmx \
-    lib/gset.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \
-    pretyping/instantiate.cmx library/libnames.cmx \
+    pretyping/recordops.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \
+    library/summary.cmi contrib/extraction/table.cmi kernel/term.cmi \
+    pretyping/termops.cmi lib/util.cmi contrib/extraction/extraction.cmi 
+contrib/extraction/extraction.cmx: kernel/declarations.cmx kernel/environ.cmx \
+    pretyping/evd.cmx library/global.cmx lib/gmap.cmx lib/gset.cmx \
+    kernel/inductive.cmx pretyping/inductiveops.cmx library/libnames.cmx \
     contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \
     library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
-    pretyping/reductionops.cmx pretyping/retyping.cmx library/summary.cmx \
-    contrib/extraction/table.cmx kernel/term.cmx pretyping/termops.cmx \
-    lib/util.cmx contrib/extraction/extraction.cmi 
+    pretyping/recordops.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \
+    library/summary.cmx contrib/extraction/table.cmx kernel/term.cmx \
+    pretyping/termops.cmx lib/util.cmx contrib/extraction/extraction.cmi 
 contrib/extraction/g_extraction.cmo: toplevel/cerrors.cmi \
     parsing/egrammar.cmi parsing/extend.cmi \
     contrib/extraction/extract_env.cmi interp/genarg.cmi parsing/pcoq.cmi \
@@ -2370,15 +2368,15 @@ contrib/extraction/mlutil.cmx: kernel/declarations.cmx library/libnames.cmx \
     contrib/extraction/miniml.cmi kernel/names.cmx library/nametab.cmx \
     lib/options.cmx lib/pp.cmx contrib/extraction/table.cmx kernel/term.cmx \
     lib/util.cmx contrib/extraction/mlutil.cmi 
-contrib/extraction/ocaml.cmo: contrib/extraction/miniml.cmi \
-    contrib/extraction/mlutil.cmi library/nameops.cmi kernel/names.cmi \
-    library/nametab.cmi lib/options.cmi lib/pp.cmi \
-    contrib/extraction/table.cmi kernel/term.cmi lib/util.cmi \
+contrib/extraction/ocaml.cmo: library/libnames.cmi \
+    contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
+    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
+    lib/pp.cmi contrib/extraction/table.cmi kernel/term.cmi lib/util.cmi \
     contrib/extraction/ocaml.cmi 
-contrib/extraction/ocaml.cmx: contrib/extraction/miniml.cmi \
-    contrib/extraction/mlutil.cmx library/nameops.cmx kernel/names.cmx \
-    library/nametab.cmx lib/options.cmx lib/pp.cmx \
-    contrib/extraction/table.cmx kernel/term.cmx lib/util.cmx \
+contrib/extraction/ocaml.cmx: library/libnames.cmx \
+    contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \
+    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
+    lib/pp.cmx contrib/extraction/table.cmx kernel/term.cmx lib/util.cmx \
     contrib/extraction/ocaml.cmi 
 contrib/extraction/scheme.cmo: contrib/extraction/miniml.cmi \
     contrib/extraction/mlutil.cmi library/nameops.cmi kernel/names.cmi \
@@ -2391,13 +2389,13 @@ contrib/extraction/scheme.cmx: contrib/extraction/miniml.cmi \
     lib/pp.cmx contrib/extraction/table.cmx kernel/term.cmx lib/util.cmx \
     contrib/extraction/scheme.cmi 
 contrib/extraction/table.cmo: kernel/declarations.cmi kernel/environ.cmi \
-    library/global.cmi library/goptions.cmi library/lib.cmi \
+    library/global.cmi lib/gmap.cmi library/goptions.cmi library/lib.cmi \
     library/libnames.cmi library/libobject.cmi kernel/names.cmi \
     library/nametab.cmi lib/options.cmi lib/pp.cmi parsing/printer.cmi \
     kernel/reduction.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \
     contrib/extraction/table.cmi 
 contrib/extraction/table.cmx: kernel/declarations.cmx kernel/environ.cmx \
-    library/global.cmx library/goptions.cmx library/lib.cmx \
+    library/global.cmx lib/gmap.cmx library/goptions.cmx library/lib.cmx \
     library/libnames.cmx library/libobject.cmx kernel/names.cmx \
     library/nametab.cmx lib/options.cmx lib/pp.cmx parsing/printer.cmx \
     kernel/reduction.cmx library/summary.cmx kernel/term.cmx lib/util.cmx \
diff --git a/.depend.coq b/.depend.coq
index 6f6be0579..6b3c3b3df 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -1,3 +1,54 @@
+theories/Reals/TypeSyntax.vo: theories/Reals/TypeSyntax.v
+theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith_base.vo theories/Reals/TypeSyntax.vo
+theories/Reals/Rsyntax.vo: theories/Reals/Rsyntax.v theories/Reals/Rdefinitions.vo
+theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rsyntax.vo theories/Reals/TypeSyntax.vo
+theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo
+theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/Rbase.vo
+theories/Reals/RealsB.vo: theories/Reals/RealsB.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo
+theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
+theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/R_Ifp.vo theories/Reals/Rbase.vo contrib/fourier/Fourier.vo
+theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rbasic_fun.vo
+theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
+theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo
+theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rlimit.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
+theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier.vo theories/Reals/SplitAbsolu.vo
+theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rfunctions.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
+theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rderiv.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
+theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rseries.vo
+theories/Reals/Alembert.vo: theories/Reals/Alembert.v theories/Arith/Max.vo theories/Reals/Raxioms.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Rtrigo_fun.vo
+theories/Reals/Binome.vo: theories/Reals/Binome.v theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Alembert.vo
+theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Binome.vo
+theories/Reals/Rcomplet.vo: theories/Reals/Rcomplet.v theories/Arith/Max.vo theories/Reals/Raxioms.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo
+theories/Reals/Alembert_compl.vo: theories/Reals/Alembert_compl.v theories/Arith/Max.vo theories/Reals/Raxioms.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Rcomplet.vo theories/Reals/Alembert.vo
+theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v theories/Arith/Even.vo theories/Arith/Div2.vo theories/Arith/Max.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Rcomplet.vo theories/Reals/Binome.vo
+theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Arith/Max.vo theories/Reals/Raxioms.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Alembert.vo theories/Reals/AltSeries.vo
+theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rcomplet.vo theories/Reals/Rtrigo_def.vo
+theories/Reals/Rprod.vo: theories/Reals/Rprod.v theories/Arith/Compare.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rtrigo_def.vo
+theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Binome.vo
+theories/Reals/Cv_prop.vo: theories/Reals/Cv_prop.v theories/Arith/Max.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/Rcomplet.vo theories/Reals/AltSeries.vo
+theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Binome.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cauchy_prod.vo
+theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Arith/Max.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Rprod.vo theories/Reals/Cv_prop.vo theories/Reals/Cos_rel.vo
+theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rfunctions.vo theories/Reals/Rsigma.vo theories/Reals/Rlimit.vo theories/Reals/Binome.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_plus.vo
+theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo
+theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/DiscrR.vo theories/Reals/Rderiv.vo theories/Reals/Alembert.vo theories/Reals/Ranalysis1.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
+theories/Reals/TAF.vo: theories/Reals/TAF.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rlimit.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo
+theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rsigma.vo theories/Reals/Alembert.vo theories/Reals/Alembert_compl.vo theories/Reals/Binome.vo theories/Reals/Cv_prop.vo theories/Reals/Rcomplet.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_plus.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo
+theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rseries.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cauchy_prod.vo theories/Reals/Binome.vo theories/Reals/Cos_plus.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo
+theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Binome.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo
+theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Rcomplet.vo theories/Reals/AltSeries.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cv_prop.vo theories/Reals/Ranalysis1.vo
+theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rsqrt_def.vo
+theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
+theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo contrib/omega/Omega.vo
+theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo
+theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rderiv.vo theories/Reals/R_sqr.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo
+theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Sqrt_reg.vo
+theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Ranalysis4.vo
+theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
+theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/DiscrR.vo theories/Reals/Rderiv.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo theories/Reals/Ranalysis4.vo theories/Reals/Rtopology.vo theories/Reals/TAF.vo
+theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rlimit.vo theories/Reals/Alembert.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo theories/Reals/NewtonInt.vo
+theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rsqrt_def.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rlimit.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Rcomplet.vo theories/Reals/Cv_prop.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Rderiv.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis4.vo theories/Reals/Exp_prop.vo theories/Reals/Rtopology.vo theories/Reals/NewtonInt.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo
+theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/AltSeries.vo theories/Reals/Rcomplet.vo theories/Reals/Rprod.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_plus.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/TAF.vo theories/Reals/Ranalysis4.vo
+theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/R_sqrt.vo theories/Reals/Rsigma.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/Rpower.vo theories/Reals/Rderiv.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rcomplet.vo theories/Reals/Alembert_compl.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Ranalysis.vo theories/Reals/Rtopology.vo theories/Reals/TAF.vo theories/Reals/NewtonInt.vo theories/Reals/DiscrR.vo theories/Reals/SplitRmult.vo theories/Reals/SplitAbsolu.vo
 theories/Init/Datatypes.vo: theories/Init/Datatypes.v
 theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v theories/Init/Datatypes.vo
 theories/Init/Peano.vo: theories/Init/Peano.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo
@@ -130,48 +181,7 @@ theories/Reals/Rsyntax.vo: theories/Reals/Rsyntax.v theories/Reals/Rdefinitions.
 theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rsyntax.vo theories/Reals/TypeSyntax.vo
 theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo
 theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/Rbase.vo
-theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
-theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/R_Ifp.vo theories/Reals/Rbase.vo contrib/fourier/Fourier.vo
-theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rbasic_fun.vo
-theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
-theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo
-theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rlimit.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
-theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier.vo theories/Reals/SplitAbsolu.vo
-theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rfunctions.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
-theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rderiv.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
-theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rseries.vo
-theories/Reals/Alembert.vo: theories/Reals/Alembert.v theories/Arith/Max.vo theories/Reals/Raxioms.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Rtrigo_fun.vo
-theories/Reals/Binome.vo: theories/Reals/Binome.v theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Alembert.vo
-theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Binome.vo
-theories/Reals/Rcomplet.vo: theories/Reals/Rcomplet.v theories/Arith/Max.vo theories/Reals/Raxioms.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo
-theories/Reals/Alembert_compl.vo: theories/Reals/Alembert_compl.v theories/Arith/Max.vo theories/Reals/Raxioms.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Rcomplet.vo theories/Reals/Alembert.vo
-theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v theories/Arith/Even.vo theories/Arith/Div2.vo theories/Arith/Max.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Rcomplet.vo theories/Reals/Binome.vo
-theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Arith/Max.vo theories/Reals/Raxioms.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Alembert.vo theories/Reals/AltSeries.vo
-theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rcomplet.vo theories/Reals/Rtrigo_def.vo
-theories/Reals/Rprod.vo: theories/Reals/Rprod.v theories/Arith/Compare.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rtrigo_def.vo
-theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Binome.vo
-theories/Reals/Cv_prop.vo: theories/Reals/Cv_prop.v theories/Arith/Max.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/Rcomplet.vo theories/Reals/AltSeries.vo
-theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Binome.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cauchy_prod.vo
-theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Arith/Max.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Rprod.vo theories/Reals/Cv_prop.vo theories/Reals/Cos_rel.vo
-theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rfunctions.vo theories/Reals/Rsigma.vo theories/Reals/Rlimit.vo theories/Reals/Binome.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_plus.vo
-theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo
-theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/DiscrR.vo theories/Reals/Rderiv.vo theories/Reals/Alembert.vo theories/Reals/Ranalysis1.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
-theories/Reals/TAF.vo: theories/Reals/TAF.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rlimit.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo
-theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rsigma.vo theories/Reals/Alembert.vo theories/Reals/Alembert_compl.vo theories/Reals/Binome.vo theories/Reals/Cv_prop.vo theories/Reals/Rcomplet.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_plus.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo
-theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rseries.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cauchy_prod.vo theories/Reals/Binome.vo theories/Reals/Cos_plus.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo
-theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Binome.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo
-theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Rcomplet.vo theories/Reals/AltSeries.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cv_prop.vo theories/Reals/Ranalysis1.vo
-theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rsqrt_def.vo
-theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
-theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo contrib/omega/Omega.vo
-theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo
-theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rderiv.vo theories/Reals/R_sqr.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo
-theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Sqrt_reg.vo
-theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Ranalysis4.vo
-theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
-theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/DiscrR.vo theories/Reals/Rderiv.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo theories/Reals/Ranalysis4.vo theories/Reals/Rtopology.vo theories/Reals/TAF.vo
-theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/AltSeries.vo theories/Reals/Rcomplet.vo theories/Reals/Rprod.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_plus.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/TAF.vo theories/Reals/Ranalysis4.vo
-theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/R_sqrt.vo theories/Reals/Rsigma.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/Rpower.vo theories/Reals/Rderiv.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rcomplet.vo theories/Reals/Alembert_compl.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Ranalysis.vo theories/Reals/Rtopology.vo theories/Reals/TAF.vo theories/Reals/NewtonInt.vo theories/Reals/DiscrR.vo theories/Reals/SplitRmult.vo theories/Reals/SplitAbsolu.vo
+theories/Reals/RealsB.vo: theories/Reals/RealsB.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo
 theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v
 theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo
 theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/PolyList.vo theories/Sets/Multiset.vo
diff --git a/Makefile b/Makefile
index f07086208..e991f9c70 100644
--- a/Makefile
+++ b/Makefile
@@ -225,8 +225,8 @@ PARSERREQUIRES=config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo \
   pretyping/indrec.cmo pretyping/pretyping.cmo \
   parsing/lexer.cmo parsing/coqast.cmo interp/genarg.cmo \
   proofs/tacexpr.cmo toplevel/vernacexpr.cmo \
-  interp/topconstr.cmo \
-  interp/ppextend.cmo interp/symbols.cmo interp/syntax_def.cmo \
+  interp/topconstr.cmo  \
+  interp/symbols.cmo interp/ppextend.cmo interp/syntax_def.cmo \
   interp/constrintern.cmo interp/coqlib.cmo \
   parsing/pcoq.cmo parsing/ast.cmo \
   parsing/extend.cmo pretyping/detyping.cmo \
@@ -554,10 +554,14 @@ WELLFOUNDEDVO=theories/Wellfounded/Disjoint_Union.vo \
 	      theories/Wellfounded/Well_Ordering.vo \
 	      theories/Wellfounded/Lexicographic_Product.vo 
 
-REALSVO=theories/Reals/TypeSyntax.vo \
+REALSBASEVO=theories/Reals/TypeSyntax.vo \
 	theories/Reals/Rdefinitions.vo theories/Reals/Rsyntax.vo \
 	theories/Reals/Raxioms.vo      theories/Reals/Rbase.vo \
-	theories/Reals/DiscrR.vo       theories/Reals/R_Ifp.vo \
+	theories/Reals/DiscrR.vo       theories/Reals/RealsB.vo \
+
+REALS_basic= 
+
+REALS_all=theories/Reals/R_Ifp.vo \
 	theories/Reals/Rbasic_fun.vo   theories/Reals/R_sqr.vo \
 	theories/Reals/SplitAbsolu.vo  theories/Reals/SplitRmult.vo \
 	theories/Reals/Rfunctions.vo   theories/Reals/Rlimit.vo \
@@ -577,8 +581,13 @@ REALSVO=theories/Reals/TypeSyntax.vo \
 	theories/Reals/Ranalysis2.vo   theories/Reals/Ranalysis3.vo \
 	theories/Reals/Sqrt_reg.vo     theories/Reals/Ranalysis4.vo \
 	theories/Reals/Ranalysis.vo    theories/Reals/Rgeom.vo \
-	theories/Reals/NewtonInt.vo \
-	theories/Reals/Rpower.vo       theories/Reals/Reals.vo 
+	theories/Reals/NewtonInt.vo    theories/Reals/RiemannInt_SF.vo \
+	theories/Reals/RiemannInt.vo   theories/Reals/Rpower.vo \
+	theories/Reals/Reals.vo 
+
+REALSVO=$(REALSBASEVO) $(REALS_$(REALS))
+
+ALLREALS=$(REALSBASEVO) $(REALS_all)
 
 SETOIDSVO=theories/Setoids/Setoid.vo
 
@@ -599,7 +608,14 @@ sets: $(SETSVO)
 intmap: $(INTMAPVO)
 relations: $(RELATIONSVO)
 wellfounded: $(WELLFOUNDEDVO)
+# reals
 reals: $(REALSVO)
+allreals: $(ALLREALS)
+install-allreals::
+	for f in $(ALLREALS); do \
+	  $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
+	  cp $$f $(FULLCOQLIB)/`dirname $$f`; \
+        done
 sorting: $(SORTINGVO)
 
 noreal: logic arith bool zarith lists sets intmap relations wellfounded sorting
@@ -1049,7 +1065,7 @@ cleanconfig::
 alldepend: depend dependcoq 
 
 dependcoq:: beforedepend
-	$(COQDEP) -R theories Coq -R contrib Coq $(COQINCLUDES) $(ALLVO:.vo=.v) > .depend.coq
+	$(COQDEP) -R theories Coq -R contrib Coq $(COQINCLUDES) $(ALLREALS:.vo=.v) $(ALLVO:.vo=.v) > .depend.coq
 
 # Build dependencies ignoring failures in building ml files from ml4 files
 # This is useful to rebuild dependencies when they are strongly corrupted:
diff --git a/config/Makefile.template b/config/Makefile.template
index 407d17012..bd7bd09d3 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -91,5 +91,8 @@ MKDIR=mkdir -p
 # Win32 systems: true (actually strip is bogus)
 STRIP=STRIPCOMMAND
 
+# Options for reals (all/basic)
+REALS=REALSOPT
+
 # make or sed are bogus and believe lines not terminating by a return
 # are inexistent
diff --git a/configure b/configure
index d4e5456d5..a534311ad 100755
--- a/configure
+++ b/configure
@@ -36,6 +36,8 @@ libdir_spec=no
 mandir_spec=no
 emacslib_spec=no
 emacs_spec=no
+reals_opt=no
+reals=all
 arch_spec=no
 
 COQTOP=`pwd`
@@ -61,7 +63,9 @@ while : ; do
                     mandir_spec=yes
 		    mandir=$COQTOP/man
                     emacslib_spec=yes
-		    emacslib=$COQTOP/tools/emacs;;
+		    emacslib=$COQTOP/tools/emacs
+		    reals_opt=yes
+		    reals=all;;
     -src|--src) COQTOP=$2
 	        shift;;
     -bindir|--bindir) bindir_spec=yes
@@ -85,6 +89,9 @@ while : ; do
     -opt|--opt) bytecamlc=ocamlc.opt
                 camlp4o=camlp4o  # can't add .opt since dyn load'll be required
                 nativecamlc=ocamlopt.opt;;
+    -reals|--reals) reals_opt=yes
+		    reals=$2
+		    shift;;
     -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
     -debug|--debug) coq_debug_flag=-g;;
     -profile|--profile) coq_profile_flag=-p;;
@@ -187,6 +194,18 @@ case $emacslib_spec in
     yes) EMACSLIB=$emacslib;;
 esac
 
+case $reals_opt in
+    no) echo "Should I compile the complete theory of real analysis [Y/N, default is Y] ?"
+	read reals_ans
+
+	case $reals_ans in
+	    "N"|"n"|"No"|"NO"|"no")
+		    reals=basic;;
+		*) true;;
+	esac;;
+    yes) true;;
+esac
+
 # case $emacs_spec in
 #     no) echo "Which Emacs command should I use to compile coq.el [$emacs_def] ?"
 #         read EMACS
@@ -315,6 +334,11 @@ echo "  Objective-Caml/Camlp4 version     : $CAMLVERSION"
 echo "  Objective-Caml/Camlp4 binaries in : $CAMLBIN"
 echo "  Objective-Caml library in         : $CAMLLIB"
 echo "  Camlp4 library in                 : $CAMLP4LIB"
+if test "$reals" = "all"; then
+echo "  Reals theory                      : All"
+else
+echo "  Reals theory                      : Basic"
+fi
 echo ""
 
 echo "  Paths for true installation:"
@@ -357,6 +381,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|BYTECAMLC|$bytecamlc|" \
     -e "s|NATIVECAMLC|$nativecamlc|" \
     -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
+    -e "s|REALSOPT|$reals|" \
       $COQTOP/config/Makefile.template > $COQTOP/config/Makefile
 
 chmod a-w $COQTOP/config/Makefile