maj

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

2 files changed, 167 insertions, 62 deletions

diff --git a/.depend b/.depend
index 603bceee1b..4ae979bef1 100644
--- a/.depend
+++ b/.depend
@@ -3784,72 +3784,176 @@ tools/coq_makefile.cmx:
 tools/coq-tex.cmo: 
 tools/coq-tex.cmx: 
 coq_fix_code.o: kernel/byterun/coq_fix_code.c \
-  /usr/local/ocaml-3.08/lib/caml/config.h \
-  /usr/local/ocaml-3.08/lib/caml/compatibility.h \
-  /usr/local/ocaml-3.08/lib/caml/misc.h \
-  /usr/local/ocaml-3.08/lib/caml/mlvalues.h \
-  /usr/local/ocaml-3.08/lib/caml/fail.h \
-  /usr/local/ocaml-3.08/lib/caml/memory.h kernel/byterun/coq_instruct.h \
-  kernel/byterun/coq_fix_code.h
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/fail.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  /home/logical/local//lib/ocaml/caml/memory.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
 coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
-  /usr/local/ocaml-3.08/lib/caml/mlvalues.h \
-  /usr/local/ocaml-3.08/lib/caml/compatibility.h \
-  /usr/local/ocaml-3.08/lib/caml/config.h \
-  /usr/local/ocaml-3.08/lib/caml/misc.h \
-  /usr/local/ocaml-3.08/lib/caml/alloc.h kernel/byterun/coq_instruct.h \
-  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
-  /usr/local/ocaml-3.08/lib/caml/fail.h \
-  /usr/local/ocaml-3.08/lib/caml/memory.h kernel/byterun/coq_values.h \
-  kernel/byterun/coq_jumptbl.h
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/alloc.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
+  kernel/byterun/coq_memory.h /home/logical/local//lib/ocaml/caml/fail.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  /home/logical/local//lib/ocaml/caml/memory.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
 coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
-  /usr/local/ocaml-3.08/lib/caml/mlvalues.h \
-  /usr/local/ocaml-3.08/lib/caml/compatibility.h \
-  /usr/local/ocaml-3.08/lib/caml/config.h \
-  /usr/local/ocaml-3.08/lib/caml/misc.h \
-  /usr/local/ocaml-3.08/lib/caml/alloc.h kernel/byterun/coq_instruct.h \
-  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
-  /usr/local/ocaml-3.08/lib/caml/fail.h \
-  /usr/local/ocaml-3.08/lib/caml/memory.h
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/alloc.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
+  kernel/byterun/coq_memory.h /home/logical/local//lib/ocaml/caml/fail.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  /home/logical/local//lib/ocaml/caml/memory.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h
 coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
-  /usr/local/ocaml-3.08/lib/caml/mlvalues.h \
-  /usr/local/ocaml-3.08/lib/caml/compatibility.h \
-  /usr/local/ocaml-3.08/lib/caml/config.h \
-  /usr/local/ocaml-3.08/lib/caml/misc.h kernel/byterun/coq_instruct.h \
-  kernel/byterun/coq_memory.h /usr/local/ocaml-3.08/lib/caml/fail.h \
-  /usr/local/ocaml-3.08/lib/caml/memory.h kernel/byterun/coq_values.h \
-  /usr/local/ocaml-3.08/lib/caml/alloc.h
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
+  /home/logical/local//lib/ocaml/caml/fail.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  /home/logical/local//lib/ocaml/caml/memory.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  kernel/byterun/coq_values.h /home/logical/local//lib/ocaml/caml/alloc.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h
 coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \
-  /usr/local/ocaml-3.08/lib/caml/config.h \
-  /usr/local/ocaml-3.08/lib/caml/compatibility.h \
-  /usr/local/ocaml-3.08/lib/caml/misc.h \
-  /usr/local/ocaml-3.08/lib/caml/mlvalues.h \
-  /usr/local/ocaml-3.08/lib/caml/fail.h \
-  /usr/local/ocaml-3.08/lib/caml/memory.h kernel/byterun/coq_instruct.h \
-  kernel/byterun/coq_fix_code.h
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/fail.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  /home/logical/local//lib/ocaml/caml/memory.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
 coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
-  /usr/local/ocaml-3.08/lib/caml/mlvalues.h \
-  /usr/local/ocaml-3.08/lib/caml/compatibility.h \
-  /usr/local/ocaml-3.08/lib/caml/config.h \
-  /usr/local/ocaml-3.08/lib/caml/misc.h \
-  /usr/local/ocaml-3.08/lib/caml/alloc.h kernel/byterun/coq_instruct.h \
-  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
-  /usr/local/ocaml-3.08/lib/caml/fail.h \
-  /usr/local/ocaml-3.08/lib/caml/memory.h kernel/byterun/coq_values.h \
-  kernel/byterun/coq_jumptbl.h
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/alloc.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
+  kernel/byterun/coq_memory.h /home/logical/local//lib/ocaml/caml/fail.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  /home/logical/local//lib/ocaml/caml/memory.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
 coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
-  /usr/local/ocaml-3.08/lib/caml/mlvalues.h \
-  /usr/local/ocaml-3.08/lib/caml/compatibility.h \
-  /usr/local/ocaml-3.08/lib/caml/config.h \
-  /usr/local/ocaml-3.08/lib/caml/misc.h \
-  /usr/local/ocaml-3.08/lib/caml/alloc.h kernel/byterun/coq_instruct.h \
-  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
-  /usr/local/ocaml-3.08/lib/caml/fail.h \
-  /usr/local/ocaml-3.08/lib/caml/memory.h
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/alloc.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
+  kernel/byterun/coq_memory.h /home/logical/local//lib/ocaml/caml/fail.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  /home/logical/local//lib/ocaml/caml/memory.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h
 coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
-  /usr/local/ocaml-3.08/lib/caml/mlvalues.h \
-  /usr/local/ocaml-3.08/lib/caml/compatibility.h \
-  /usr/local/ocaml-3.08/lib/caml/config.h \
-  /usr/local/ocaml-3.08/lib/caml/misc.h kernel/byterun/coq_instruct.h \
-  kernel/byterun/coq_memory.h /usr/local/ocaml-3.08/lib/caml/fail.h \
-  /usr/local/ocaml-3.08/lib/caml/memory.h kernel/byterun/coq_values.h \
-  /usr/local/ocaml-3.08/lib/caml/alloc.h
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
+  /home/logical/local//lib/ocaml/caml/fail.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  /home/logical/local//lib/ocaml/caml/memory.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/config.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h \
+  kernel/byterun/coq_values.h /home/logical/local//lib/ocaml/caml/alloc.h \
+  /home/logical/local//lib/ocaml/caml/compatibility.h \
+  /home/logical/local//lib/ocaml/caml/misc.h \
+  /home/logical/local//lib/ocaml/caml/mlvalues.h
diff --git a/.depend.coq b/.depend.coq
index 3002ddbe03..cc531c7b04 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -279,3 +279,4 @@ contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/R
 contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo contrib/field/field.cmo contrib/fourier/Fourier_util.vo contrib/field/Field.vo theories/Reals/DiscrR.vo
 contrib/rtauto/Bintree.vo: contrib/rtauto/Bintree.v theories/Lists/List.vo theories/NArith/BinPos.vo
 contrib/rtauto/Rtauto.vo: contrib/rtauto/Rtauto.v theories/Lists/List.vo contrib/rtauto/Bintree.vo theories/Bool/Bool.vo theories/NArith/BinPos.vo
+contrib/recdef/Recdef.vo: contrib/recdef/Recdef.v theories/Arith/Arith.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo contrib/recdef/recdef.cmo