From b6f207f5948b8bb1681c933f8f43411203586672 Mon Sep 17 00:00:00 2001 From: barras Date: Tue, 26 Sep 2006 16:38:33 +0000 Subject: petits pbs de dependances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9181 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 112 +++++++++++++++++++--------------------- .depend.coq | 10 ++-- Makefile | 22 ++++---- contrib/ring/LegacyZArithRing.v | 2 +- 4 files changed, 69 insertions(+), 77 deletions(-) diff --git a/.depend b/.depend index 1e730c2d0..18778724d 100644 --- a/.depend +++ b/.depend @@ -4109,74 +4109,66 @@ tools/coq_makefile.cmx: tools/coq-tex.cmo: tools/coq-tex.cmx: coq_fix_code.o: kernel/byterun/coq_fix_code.c \ - /usr/lib/ocaml/3.09.2/caml/config.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/config.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/fail.h /usr/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_instruct.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/misc.h /usr/lib/ocaml/caml/config.h \ + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/mlvalues.h \ + /usr/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/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/alloc.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \ - /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h \ - kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ + kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \ + /usr/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/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/alloc.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \ - /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ + kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/memory.h coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \ + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_values.h \ - /usr/lib/ocaml/3.09.2/caml/alloc.h + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/fail.h \ + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + /usr/lib/ocaml/caml/alloc.h coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \ - /usr/lib/ocaml/3.09.2/caml/config.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/config.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/fail.h /usr/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_instruct.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/misc.h /usr/lib/ocaml/caml/config.h \ + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/mlvalues.h \ + /usr/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/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/alloc.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \ - /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h \ - kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ + kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \ + /usr/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/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/alloc.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \ - /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ + kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \ + /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/memory.h coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \ + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \ + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_values.h \ - /usr/lib/ocaml/3.09.2/caml/alloc.h + /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/fail.h \ + /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \ + /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + /usr/lib/ocaml/caml/alloc.h diff --git a/.depend.coq b/.depend.coq index f15ba9f2d..9d2f498e6 100644 --- a/.depend.coq +++ b/.depend.coq @@ -342,7 +342,7 @@ contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Legac contrib/ring/LegacyRing_theory.vo: contrib/ring/LegacyRing_theory.v theories/Bool/Bool.vo contrib/ring/LegacyRing.vo: contrib/ring/LegacyRing.v theories/Bool/Bool.vo contrib/ring/LegacyRing_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_abstract.vo contrib/ring/LegacyNArithRing.vo: contrib/ring/LegacyNArithRing.v theories/Bool/Bool.vo contrib/ring/LegacyRing.vo theories/ZArith/ZArith_base.vo theories/NArith/NArith.vo theories/Logic/Eqdep_dec.vo -contrib/ring/LegacyZArithRing.vo: contrib/ring/LegacyZArithRing.v contrib/setoid_ring/ArithRing.vo theories/ZArith/ZArith_base.vo theories/Logic/Eqdep_dec.vo +contrib/ring/LegacyZArithRing.vo: contrib/ring/LegacyZArithRing.v contrib/ring/LegacyArithRing.vo theories/ZArith/ZArith_base.vo theories/Logic/Eqdep_dec.vo contrib/ring/LegacyRing.vo contrib/ring/Ring_abstract.vo: contrib/ring/Ring_abstract.v contrib/ring/LegacyRing_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Quote.vo: contrib/ring/Quote.v contrib/ring/Setoid_ring_normalize.vo: contrib/ring/Setoid_ring_normalize.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo @@ -360,13 +360,15 @@ contrib/rtauto/Bintree.vo: contrib/rtauto/Bintree.v theories/Lists/List.vo theor 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/Compare_dec.vo theories/Arith/Wf_nat.vo contrib/setoid_ring/BinList.vo: contrib/setoid_ring/BinList.v theories/NArith/BinPos.vo theories/Lists/List.vo +contrib/setoid_ring/Ring_theory.vo: contrib/setoid_ring/Ring_theory.v theories/Setoids/Setoid.vo +contrib/setoid_ring/Ring_polynom.vo: contrib/setoid_ring/Ring_polynom.v theories/Setoids/Setoid.vo contrib/setoid_ring/BinList.vo theories/NArith/BinPos.vo theories/ZArith/BinInt.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_tac.vo: contrib/setoid_ring/Ring_tac.v theories/Setoids/Setoid.vo theories/NArith/BinPos.vo contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/BinList.vo contrib/setoid_ring/newring.cmo -contrib/setoid_ring/Ring_equiv.vo: contrib/setoid_ring/Ring_equiv.v contrib/ring/Setoid_ring_theory.vo contrib/ring/LegacyRing_theory.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_base.vo: contrib/setoid_ring/Ring_base.v contrib/setoid_ring/newring.cmo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_tac.vo +contrib/setoid_ring/InitialRing.vo: contrib/setoid_ring/InitialRing.v theories/ZArith/ZArith_base.vo theories/ZArith/BinInt.vo theories/NArith/BinNat.vo theories/Setoids/Setoid.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/Ring_polynom.vo +contrib/setoid_ring/Ring_equiv.vo: contrib/setoid_ring/Ring_equiv.v contrib/ring/Setoid_ring_theory.vo contrib/ring/LegacyRing_theory.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring.vo: contrib/setoid_ring/Ring.v theories/Bool/Bool.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Ring_equiv.vo contrib/setoid_ring/ArithRing.vo: contrib/setoid_ring/ArithRing.v theories/Arith/Arith.vo contrib/setoid_ring/Ring.vo -contrib/setoid_ring/Ring_polynom.vo: contrib/setoid_ring/Ring_polynom.v theories/Setoids/Setoid.vo contrib/setoid_ring/BinList.vo theories/NArith/BinPos.vo theories/ZArith/BinInt.vo contrib/setoid_ring/Ring_theory.vo -contrib/setoid_ring/NArithRing.vo: contrib/setoid_ring/NArithRing.v theories/NArith/NArith.vo contrib/setoid_ring/Ring.vo +contrib/setoid_ring/NArithRing.vo: contrib/setoid_ring/NArithRing.v theories/NArith/NArith.vo contrib/setoid_ring/Ring.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/ZArithRing.vo: contrib/setoid_ring/ZArithRing.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo contrib/setoid_ring/Field.vo: contrib/setoid_ring/Field.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo contrib/setoid_ring/Field_tac.vo: contrib/setoid_ring/Field_tac.v contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Field.vo diff --git a/Makefile b/Makefile index 85c8efde0..2aa278c8e 100644 --- a/Makefile +++ b/Makefile @@ -1042,22 +1042,20 @@ RINGVO=\ contrib/ring/Quote.vo contrib/ring/Setoid_ring_normalize.vo \ contrib/ring/Setoid_ring.vo contrib/ring/Setoid_ring_theory.vo -NEWRINGVO=\ - contrib/setoid_ring/BinList.vo contrib/setoid_ring/Ring_th.vo \ - contrib/setoid_ring/Pol.vo contrib/setoid_ring/Ring_tac.vo \ - contrib/setoid_ring/ZRing_th.vo contrib/setoid_ring/Ring_equiv.vo \ - contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/Ring.vo \ - contrib/setoid_ring/ArithRing.vo contrib/setoid_ring/Ring_polynom.vo \ - contrib/setoid_ring/NArithRing.vo \ - contrib/setoid_ring/ZArithRing.vo \ -contrib/setoid_ring/Field.vo \ -contrib/setoid_ring/Field_tac.vo \ -contrib/setoid_ring/RealField.vo - FIELDVO=\ contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo \ contrib/field/Field_Tactic.vo contrib/field/LegacyField.vo +NEWRINGVO=\ + contrib/setoid_ring/BinList.vo contrib/setoid_ring/Ring_theory.vo \ + contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/Ring_tac.vo \ + contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/InitialRing.vo \ + contrib/setoid_ring/Ring_equiv.vo contrib/setoid_ring/Ring.vo \ + contrib/setoid_ring/ArithRing.vo contrib/setoid_ring/NArithRing.vo \ + contrib/setoid_ring/ZArithRing.vo \ + contrib/setoid_ring/Field.vo contrib/setoid_ring/Field_tac.vo \ + contrib/setoid_ring/RealField.vo + XMLVO= FOURIERVO=\ diff --git a/contrib/ring/LegacyZArithRing.v b/contrib/ring/LegacyZArithRing.v index 9669d4f86..68a0dd275 100644 --- a/contrib/ring/LegacyZArithRing.v +++ b/contrib/ring/LegacyZArithRing.v @@ -10,7 +10,7 @@ (* Instantiation of the Ring tactic for the binary integers of ZArith *) -Require Export ArithRing. +Require Export LegacyArithRing. Require Export ZArith_base. Require Import Eqdep_dec. Require Import LegacyRing. -- cgit v1.2.3