From 2f8968f4766c325b22b8ebfecec087d8cc4f0508 Mon Sep 17 00:00:00 2001 From: coq Date: Wed, 11 Jan 2006 23:36:07 +0000 Subject: maj git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7852 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 160 +++++++++++++++++++++++++++++++++++------------------------- make.result | 2 +- 2 files changed, 95 insertions(+), 67 deletions(-) diff --git a/.depend b/.depend index dfe57dcdb..1a060993e 100644 --- a/.depend +++ b/.depend @@ -642,13 +642,13 @@ interp/syntax_def.cmx: lib/util.cmx interp/topconstr.cmx library/summary.cmx \ kernel/names.cmx library/nameops.cmx library/libobject.cmx \ library/libnames.cmx library/lib.cmx interp/syntax_def.cmi interp/topconstr.cmo: lib/util.cmi kernel/term.cmi pretyping/rawterm.cmi \ - lib/pp.cmi lib/options.cmi kernel/names.cmi library/nameops.cmi \ - kernel/mod_subst.cmi library/libnames.cmi pretyping/evd.cmi lib/dyn.cmi \ - pretyping/detyping.cmi lib/bigint.cmi interp/topconstr.cmi + lib/pp.cmi kernel/names.cmi library/nameops.cmi kernel/mod_subst.cmi \ + library/libnames.cmi pretyping/evd.cmi lib/dyn.cmi pretyping/detyping.cmi \ + lib/bigint.cmi interp/topconstr.cmi interp/topconstr.cmx: lib/util.cmx kernel/term.cmx pretyping/rawterm.cmx \ - lib/pp.cmx lib/options.cmx kernel/names.cmx library/nameops.cmx \ - kernel/mod_subst.cmx library/libnames.cmx pretyping/evd.cmx lib/dyn.cmx \ - pretyping/detyping.cmx lib/bigint.cmx interp/topconstr.cmi + lib/pp.cmx kernel/names.cmx library/nameops.cmx kernel/mod_subst.cmx \ + library/libnames.cmx pretyping/evd.cmx lib/dyn.cmx pretyping/detyping.cmx \ + lib/bigint.cmx interp/topconstr.cmi kernel/cbytecodes.cmo: kernel/term.cmi kernel/names.cmi kernel/cbytecodes.cmi kernel/cbytecodes.cmx: kernel/term.cmx kernel/names.cmx kernel/cbytecodes.cmi kernel/cbytegen.cmo: lib/util.cmi kernel/term.cmi kernel/pre_env.cmi \ @@ -2035,6 +2035,8 @@ tactics/termdn.cmx: lib/util.cmx kernel/term.cmx pretyping/rawterm.cmx \ pretyping/pattern.cmx library/nametab.cmx kernel/names.cmx \ library/nameops.cmx library/libnames.cmx tactics/dn.cmx \ tactics/termdn.cmi +test-suite/zarith.cmo: test-suite/zarith.cmi +test-suite/zarith.cmx: test-suite/zarith.cmi tools/coqdep.cmo: tools/coqdep_lexer.cmo config/coq_config.cmi tools/coqdep.cmx: tools/coqdep_lexer.cmx config/coq_config.cmx tools/gallina.cmo: tools/gallina_lexer.cmo @@ -3467,8 +3469,6 @@ tools/coqdoc/pretty.cmo: tools/coqdoc/output.cmi tools/coqdoc/index.cmi \ tools/coqdoc/pretty.cmi tools/coqdoc/pretty.cmx: tools/coqdoc/output.cmx tools/coqdoc/index.cmx \ tools/coqdoc/pretty.cmi -tools/coqdoc/theory.cmo: tools/coqdoc/output.cmi -tools/coqdoc/theory.cmx: tools/coqdoc/output.cmx tactics/tauto.cmo: parsing/grammar.cma tactics/tauto.cmx: parsing/grammar.cma tactics/eqdecide.cmo: parsing/grammar.cma @@ -3570,74 +3570,102 @@ tools/coq_makefile.cmx: tools/coq-tex.cmo: tools/coq-tex.cmx: coq_fix_code.o: kernel/byterun/coq_fix_code.c \ - /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/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/config.h \ + /home/logical/local//lib/ocaml/caml/mlvalues.h \ + /home/logical/local//lib/ocaml/caml/misc.h \ + /home/logical/local//lib/ocaml/caml/fail.h \ + /home/logical/local//lib/ocaml/caml/mlvalues.h \ + /home/logical/local//lib/ocaml/caml/memory.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/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.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/alloc.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 /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - kernel/byterun/coq_jumptbl.h + kernel/byterun/coq_memory.h \ + /home/logical/local//lib/ocaml/caml/config.h \ + /home/logical/local//lib/ocaml/caml/fail.h \ + /home/logical/local//lib/ocaml/caml/misc.h \ + /home/logical/local//lib/ocaml/caml/memory.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/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.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/alloc.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 /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h + kernel/byterun/coq_memory.h \ + /home/logical/local//lib/ocaml/caml/config.h \ + /home/logical/local//lib/ocaml/caml/fail.h \ + /home/logical/local//lib/ocaml/caml/misc.h \ + /home/logical/local//lib/ocaml/caml/memory.h coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.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 \ kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \ - /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - /usr/local/lib/ocaml/caml/alloc.h + /home/logical/local//lib/ocaml/caml/config.h \ + /home/logical/local//lib/ocaml/caml/fail.h \ + /home/logical/local//lib/ocaml/caml/mlvalues.h \ + /home/logical/local//lib/ocaml/caml/misc.h \ + /home/logical/local//lib/ocaml/caml/memory.h \ + kernel/byterun/coq_values.h /home/logical/local//lib/ocaml/caml/alloc.h coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \ - /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/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/config.h \ + /home/logical/local//lib/ocaml/caml/mlvalues.h \ + /home/logical/local//lib/ocaml/caml/misc.h \ + /home/logical/local//lib/ocaml/caml/fail.h \ + /home/logical/local//lib/ocaml/caml/mlvalues.h \ + /home/logical/local//lib/ocaml/caml/memory.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/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.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/alloc.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 /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - kernel/byterun/coq_jumptbl.h + kernel/byterun/coq_memory.h \ + /home/logical/local//lib/ocaml/caml/config.h \ + /home/logical/local//lib/ocaml/caml/fail.h \ + /home/logical/local//lib/ocaml/caml/misc.h \ + /home/logical/local//lib/ocaml/caml/memory.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/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.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/alloc.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 /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h + kernel/byterun/coq_memory.h \ + /home/logical/local//lib/ocaml/caml/config.h \ + /home/logical/local//lib/ocaml/caml/fail.h \ + /home/logical/local//lib/ocaml/caml/misc.h \ + /home/logical/local//lib/ocaml/caml/memory.h coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.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 \ kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \ - /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - /usr/local/lib/ocaml/caml/alloc.h + /home/logical/local//lib/ocaml/caml/config.h \ + /home/logical/local//lib/ocaml/caml/fail.h \ + /home/logical/local//lib/ocaml/caml/mlvalues.h \ + /home/logical/local//lib/ocaml/caml/misc.h \ + /home/logical/local//lib/ocaml/caml/memory.h \ + kernel/byterun/coq_values.h /home/logical/local//lib/ocaml/caml/alloc.h diff --git a/make.result b/make.result index 420d3cb19..639398fec 100644 --- a/make.result +++ b/make.result @@ -1 +1 @@ -Wed 11/01/2006 00:30: Success +Thu 12/01/2006 00:30: Success -- cgit v1.2.3