From 844624640d335bd49bc187a135548734ea353e37 Mon Sep 17 00:00:00 2001 From: filliatr Date: Thu, 26 Aug 1999 09:59:36 +0000 Subject: le noyau compile et link git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@26 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .cvsignore | 1 + .depend | 85 ++++++++++++++++++++++++++++++++--------------------- Makefile | 9 +++--- dev/changements.txt | 1 + 4 files changed, 58 insertions(+), 38 deletions(-) create mode 100644 .cvsignore diff --git a/.cvsignore b/.cvsignore new file mode 100644 index 0000000000..6443d52fdd --- /dev/null +++ b/.cvsignore @@ -0,0 +1 @@ +coqtop.byte diff --git a/.depend b/.depend index e8c5c9eb05..1f8d5b95c4 100644 --- a/.depend +++ b/.depend @@ -1,3 +1,7 @@ +attente/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ + kernel/sign.cmi kernel/term.cmi +attente/printer.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ + kernel/sign.cmi kernel/term.cmi kernel/abstraction.cmi: kernel/names.cmi kernel/term.cmi kernel/closure.cmi: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ kernel/names.cmi lib/pp.cmi kernel/term.cmi @@ -6,8 +10,6 @@ kernel/environ.cmi: kernel/constant.cmi kernel/evd.cmi kernel/inductive.cmi \ kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi kernel/evd.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/generic.cmi: kernel/names.cmi lib/util.cmi -kernel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ - kernel/sign.cmi kernel/term.cmi kernel/inductive.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/instantiate.cmi: kernel/environ.cmi kernel/names.cmi kernel/term.cmi kernel/mach.cmi: kernel/environ.cmi kernel/machops.cmi kernel/names.cmi \ @@ -15,27 +17,36 @@ kernel/mach.cmi: kernel/environ.cmi kernel/machops.cmi kernel/names.cmi \ kernel/machops.cmi: kernel/environ.cmi kernel/names.cmi kernel/term.cmi \ kernel/univ.cmi kernel/names.cmi: lib/pp.cmi -kernel/printer.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ - kernel/sign.cmi kernel/term.cmi kernel/reduction.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/generic.cmi kernel/names.cmi kernel/term.cmi kernel/univ.cmi kernel/sign.cmi: kernel/generic.cmi kernel/names.cmi kernel/term.cmi +kernel/sosub.cmi: kernel/term.cmi kernel/term.cmi: lib/coqast.cmi kernel/generic.cmi kernel/names.cmi \ kernel/univ.cmi +kernel/type_errors.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ + kernel/sign.cmi kernel/term.cmi kernel/univ.cmi: kernel/names.cmi lib/coqast.cmi: lib/dyn.cmi lib/pp.cmi: lib/pp_control.cmi lib/util.cmi: lib/pp.cmi +attente/himsg.cmo: kernel/environ.cmi kernel/generic.cmi lib/pp.cmi \ + kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi \ + attente/himsg.cmi +attente/himsg.cmx: kernel/environ.cmx kernel/generic.cmx lib/pp.cmx \ + kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx lib/util.cmx \ + attente/himsg.cmi config/coq_config.cmo: config/coq_config.cmi config/coq_config.cmx: config/coq_config.cmi +kernel/abstraction.cmo: kernel/generic.cmi kernel/names.cmi kernel/sosub.cmi \ + kernel/term.cmi lib/util.cmi kernel/abstraction.cmi +kernel/abstraction.cmx: kernel/generic.cmx kernel/names.cmx kernel/sosub.cmx \ + kernel/term.cmx lib/util.cmx kernel/abstraction.cmi kernel/closure.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \ - kernel/printer.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \ - kernel/closure.cmi + kernel/term.cmi kernel/univ.cmi lib/util.cmi kernel/closure.cmi kernel/closure.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \ - kernel/printer.cmi kernel/term.cmx kernel/univ.cmi lib/util.cmx \ - kernel/closure.cmi + kernel/term.cmx kernel/univ.cmx lib/util.cmx kernel/closure.cmi kernel/constant.cmo: kernel/generic.cmi kernel/names.cmi kernel/sign.cmi \ kernel/term.cmi kernel/constant.cmi kernel/constant.cmx: kernel/generic.cmx kernel/names.cmx kernel/sign.cmx \ @@ -43,9 +54,9 @@ kernel/constant.cmx: kernel/generic.cmx kernel/names.cmx kernel/sign.cmx \ kernel/environ.cmo: kernel/abstraction.cmi kernel/constant.cmi kernel/evd.cmi \ kernel/generic.cmi kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi \ kernel/term.cmi kernel/univ.cmi lib/util.cmi kernel/environ.cmi -kernel/environ.cmx: kernel/abstraction.cmi kernel/constant.cmx kernel/evd.cmx \ +kernel/environ.cmx: kernel/abstraction.cmx kernel/constant.cmx kernel/evd.cmx \ kernel/generic.cmx kernel/inductive.cmx kernel/names.cmx kernel/sign.cmx \ - kernel/term.cmx kernel/univ.cmi lib/util.cmx kernel/environ.cmi + kernel/term.cmx kernel/univ.cmx lib/util.cmx kernel/environ.cmi kernel/evd.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi \ kernel/evd.cmi kernel/evd.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx lib/util.cmx \ @@ -54,12 +65,6 @@ kernel/generic.cmo: kernel/names.cmi lib/pp.cmi lib/util.cmi \ kernel/generic.cmi kernel/generic.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx \ kernel/generic.cmi -kernel/himsg.cmo: kernel/environ.cmi kernel/generic.cmi lib/pp.cmi \ - kernel/printer.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \ - lib/util.cmi kernel/himsg.cmi -kernel/himsg.cmx: kernel/environ.cmx kernel/generic.cmx lib/pp.cmx \ - kernel/printer.cmi kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ - lib/util.cmx kernel/himsg.cmi kernel/inductive.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \ kernel/inductive.cmi kernel/inductive.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx \ @@ -70,42 +75,54 @@ kernel/instantiate.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/instantiate.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \ kernel/generic.cmx kernel/names.cmx lib/pp.cmx kernel/sign.cmx \ kernel/term.cmx lib/util.cmx kernel/instantiate.cmi -kernel/mach.cmo: kernel/environ.cmi kernel/generic.cmi kernel/himsg.cmi \ - kernel/machops.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \ - kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \ +kernel/mach.cmo: kernel/environ.cmi kernel/generic.cmi kernel/machops.cmi \ + kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/type_errors.cmi kernel/univ.cmi lib/util.cmi \ kernel/mach.cmi -kernel/mach.cmx: kernel/environ.cmx kernel/generic.cmx kernel/himsg.cmx \ - kernel/machops.cmx kernel/names.cmx lib/pp.cmx kernel/reduction.cmx \ - kernel/sign.cmx kernel/term.cmx kernel/univ.cmi lib/util.cmx \ +kernel/mach.cmx: kernel/environ.cmx kernel/generic.cmx kernel/machops.cmx \ + kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \ + kernel/term.cmx kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx \ kernel/mach.cmi kernel/machops.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \ - kernel/generic.cmi kernel/himsg.cmi kernel/inductive.cmi \ - kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \ - kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \ + kernel/generic.cmi kernel/inductive.cmi kernel/instantiate.cmi \ + kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/type_errors.cmi kernel/univ.cmi lib/util.cmi \ kernel/machops.cmi kernel/machops.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \ - kernel/generic.cmx kernel/himsg.cmx kernel/inductive.cmx \ - kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/reduction.cmx \ - kernel/sign.cmx kernel/term.cmx kernel/univ.cmi lib/util.cmx \ + kernel/generic.cmx kernel/inductive.cmx kernel/instantiate.cmx \ + kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \ + kernel/term.cmx kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx \ kernel/machops.cmi kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/util.cmi kernel/names.cmi kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/util.cmx kernel/names.cmi kernel/reduction.cmo: kernel/closure.cmi kernel/constant.cmi \ kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi kernel/inductive.cmi \ - kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/printer.cmi \ - kernel/term.cmi kernel/univ.cmi lib/util.cmi kernel/reduction.cmi + kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \ + kernel/univ.cmi lib/util.cmi kernel/reduction.cmi kernel/reduction.cmx: kernel/closure.cmx kernel/constant.cmx \ kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx kernel/inductive.cmx \ - kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/printer.cmi \ - kernel/term.cmx kernel/univ.cmi lib/util.cmx kernel/reduction.cmi + kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \ + kernel/univ.cmx lib/util.cmx kernel/reduction.cmi kernel/sign.cmo: kernel/generic.cmi kernel/names.cmi kernel/term.cmi \ lib/util.cmi kernel/sign.cmi kernel/sign.cmx: kernel/generic.cmx kernel/names.cmx kernel/term.cmx \ lib/util.cmx kernel/sign.cmi +kernel/sosub.cmo: kernel/generic.cmi kernel/names.cmi kernel/term.cmi \ + lib/util.cmi kernel/sosub.cmi +kernel/sosub.cmx: kernel/generic.cmx kernel/names.cmx kernel/term.cmx \ + lib/util.cmx kernel/sosub.cmi kernel/term.cmo: lib/coqast.cmi kernel/generic.cmi lib/hashcons.cmi \ kernel/names.cmi lib/pp.cmi kernel/univ.cmi lib/util.cmi kernel/term.cmi -kernel/term.cmx: lib/coqast.cmi kernel/generic.cmx lib/hashcons.cmx \ - kernel/names.cmx lib/pp.cmx kernel/univ.cmi lib/util.cmx kernel/term.cmi +kernel/term.cmx: lib/coqast.cmx kernel/generic.cmx lib/hashcons.cmx \ + kernel/names.cmx lib/pp.cmx kernel/univ.cmx lib/util.cmx kernel/term.cmi +kernel/type_errors.cmo: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ + kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi +kernel/type_errors.cmx: kernel/environ.cmx kernel/names.cmx lib/pp.cmx \ + kernel/sign.cmx kernel/term.cmx kernel/type_errors.cmi +kernel/univ.cmo: kernel/names.cmi lib/pp.cmi lib/util.cmi kernel/univ.cmi +kernel/univ.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx kernel/univ.cmi +lib/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi lib/coqast.cmi +lib/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx lib/coqast.cmi lib/dyn.cmo: lib/util.cmi lib/dyn.cmi lib/dyn.cmx: lib/util.cmx lib/dyn.cmi lib/hashcons.cmo: lib/hashcons.cmi diff --git a/Makefile b/Makefile index 331f8080fc..d33ff7060d 100644 --- a/Makefile +++ b/Makefile @@ -23,20 +23,21 @@ INCLUDES=-I config -I lib -I kernel CONFIG=config/coq_config.cmo LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/hashcons.cmo \ - lib/dyn.cmo + lib/dyn.cmo lib/coqast.cmo -KERNEL=kernel/names.cmo kernel/generic.cmo kernel/term.cmo \ +KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \ kernel/sign.cmo kernel/evd.cmo kernel/constant.cmo \ - kernel/inductive.cmo \ + kernel/inductive.cmo kernel/sosub.cmo kernel/abstraction.cmo \ kernel/environ.cmo kernel/instantiate.cmo \ kernel/closure.cmo kernel/reduction.cmo \ - kernel/himsg.cmo kernel/machops.cmo kernel/mach.cmo + kernel/type_errors.cmo kernel/machops.cmo kernel/mach.cmo OBJS=$(CONFIG) $(LIB) $(KERNEL) # Targets world: $(OBJS) + $(OCAMLC) -o coqtop.byte $(OBJS) # Literate programming (with ocamlweb) diff --git a/dev/changements.txt b/dev/changements.txt index 09c0a7b6f5..424132329b 100644 --- a/dev/changements.txt +++ b/dev/changements.txt @@ -34,6 +34,7 @@ Changements dans les fonctions : cons_vect -> array_cons map_i_vect -> Array.mapi map2_vect -> array_map2 + list_of_tl_vect -> array_list_of_tl Std comp -> Util.compose -- cgit v1.2.3