diff options
| author | filliatr | 1999-08-17 14:06:06 +0000 |
|---|---|---|
| committer | filliatr | 1999-08-17 14:06:06 +0000 |
| commit | ff3f2da65bb4033b4f60fe3890d5392315fe09b5 (patch) | |
| tree | 2f25612a1e914175566ac89b506573a1b2921ae8 | |
| parent | c85ed98ae100c524bb572ebbfd2f4228a11932be (diff) | |
ajout de modules
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | .depend | 28 | ||||
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | dev/changements.txt | 26 |
3 files changed, 55 insertions, 5 deletions
@@ -1,12 +1,36 @@ +kernel/environ.cmi: kernel/names.cmi kernel/term.cmi +kernel/evd.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi +kernel/generic.cmi: kernel/names.cmi lib/util.cmi kernel/names.cmi: lib/pp.cmi +kernel/sign.cmi: kernel/generic.cmi kernel/names.cmi kernel/term.cmi +kernel/term.cmi: lib/coqast.cmi kernel/generic.cmi kernel/names.cmi \ + kernel/univ.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 config/coq_config.cmo: config/coq_config.cmi config/coq_config.cmx: config/coq_config.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 \ + kernel/evd.cmi +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/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/sign.cmo: kernel/sign.cmi -kernel/sign.cmx: kernel/sign.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/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 +lib/dyn.cmo: lib/util.cmi lib/dyn.cmi +lib/dyn.cmx: lib/util.cmx lib/dyn.cmi lib/hashcons.cmo: lib/hashcons.cmi lib/hashcons.cmx: lib/hashcons.cmi lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi @@ -22,9 +22,11 @@ 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=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/hashcons.cmo \ + lib/dyn.cmo -KERNEL=kernel/names.cmo kernel/sign.cmo +KERNEL=kernel/names.cmo kernel/generic.cmo kernel/term.cmo \ + kernel/sign.cmo kernel/evd.cmo OBJS=$(CONFIG) $(LIB) $(KERNEL) diff --git a/dev/changements.txt b/dev/changements.txt index 5a190073fa..f0f25bba8a 100644 --- a/dev/changements.txt +++ b/dev/changements.txt @@ -1,5 +1,6 @@ -Voici les changements d'organisation / modules : +Changements d'organisation / modules : +-------------------------------------- AVANT APRÈS ================================ =============================== @@ -8,3 +9,26 @@ Voici les changements d'organisation / modules : Names kernel/names.ml et kernel/sign.ml (les parties noms et signatures ont été séparées) + + +Changements dans les types de données : +--------------------------------------- + dans Generic: free_rels : constr -> int Listset.t + devient : constr -> Intset.t + +Changements dans les fonctions : +-------------------------------- + + Vectops. + it_vect -> Array.fold_left + vect_it -> Array.fold_right + exists_vect -> Util.array_exists + for_all2eq_vect -> Util.array_for_all2 + tabulate_vect -> Array.init + hd_vect -> Util.array_hd + it_vect_from -> array_fold_left_from + vect_it_from -> array_fold_right_from + app_tl_vect -> array_app_tl + cons_vect -> array_cons + + Std.comp -> Util.compose |