diff options
| -rw-r--r-- | .depend | 20 | ||||
| -rw-r--r-- | .depend.coq | 9 |
2 files changed, 18 insertions, 11 deletions
@@ -2195,17 +2195,17 @@ toplevel/toplevel.cmx: toplevel/cerrors.cmx library/lib.cmx \ toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi toplevel/vernac.cmo: interp/constrextern.cmi interp/constrintern.cmi \ - parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \ - kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \ - lib/pp.cmi translate/ppvernacnew.cmi library/states.cmi lib/system.cmi \ - lib/util.cmi toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \ - toplevel/vernacinterp.cmi toplevel/vernac.cmi + parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/libnames.cmi \ + library/library.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \ + proofs/pfedit.cmi lib/pp.cmi translate/ppvernacnew.cmi library/states.cmi \ + lib/system.cmi lib/util.cmi toplevel/vernacentries.cmi \ + toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \ - parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \ - kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \ - lib/pp.cmx translate/ppvernacnew.cmx library/states.cmx lib/system.cmx \ - lib/util.cmx toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \ - toplevel/vernacinterp.cmx toplevel/vernac.cmi + parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/libnames.cmx \ + library/library.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \ + proofs/pfedit.cmx lib/pp.cmx translate/ppvernacnew.cmx library/states.cmx \ + lib/system.cmx lib/util.cmx toplevel/vernacentries.cmx \ + toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \ pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \ interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \ diff --git a/.depend.coq b/.depend.coq index f24c76f709..fb8ddd00ca 100644 --- a/.depend.coq +++ b/.depend.coq @@ -60,6 +60,14 @@ theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Notations.vo theor theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Notations.vo theories/Init/Logic.vo theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Notations.vo theories/Init/Logic.vo theories/Init/Datatypes.vo theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Notations.vo theories/Init/Datatypes.vo theories/Init/Logic.vo theories/Init/Specif.vo theories/Init/Peano.vo theories/Init/Wf.vo +theories/Init/Notations.vo: theories/Init/Notations.v +theories/Init/Datatypes.vo: theories/Init/Datatypes.v theories/Init/Notations.vo +theories/Init/Peano.vo: theories/Init/Peano.v theories/Init/Notations.vo theories/Init/Datatypes.vo theories/Init/Logic.vo +theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Notations.vo theories/Init/Datatypes.vo +theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Notations.vo theories/Init/Datatypes.vo theories/Init/Logic.vo +theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Notations.vo theories/Init/Logic.vo +theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Notations.vo theories/Init/Logic.vo theories/Init/Datatypes.vo +theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Notations.vo theories/Init/Datatypes.vo theories/Init/Logic.vo theories/Init/Specif.vo theories/Init/Peano.vo theories/Init/Wf.vo theories/Logic/Hurkens.vo: theories/Logic/Hurkens.v theories/Logic/ProofIrrelevance.vo: theories/Logic/ProofIrrelevance.v theories/Logic/Hurkens.vo theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo @@ -263,5 +271,4 @@ contrib/correctness/Sorted.vo: contrib/correctness/Sorted.v contrib/correctness/ contrib/correctness/Tuples.vo: contrib/correctness/Tuples.v contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo 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/interface/Centaur.vo: contrib/interface/Centaur.v contrib/cc/CC.vo: contrib/cc/CC.v theories/Logic/Eqdep_dec.vo |