]> matita.cs.unibo.it Git - helm.git/commit
1) NCicLibrary (which is untrusted) moved after NCicUntrusted.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 16 Jun 2009 22:35:03 +0000 (22:35 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 16 Jun 2009 22:35:03 +0000 (22:35 +0000)
commit134d8273511016e9b6de3423d301a080046f3948
tree6d3bd437101e1568ebf969b355469deb700a7856
parent33435f271509f4888d44f9446b078eeebbe71519
1) NCicLibrary (which is untrusted) moved after NCicUntrusted.
   NCicLibrary registers get_obj to NCicEnvironemnt (and to NCicPp)
2) URIs are now refreshed when objects are included from disk

Observation: even NCicPp is untrusted. Thus its implementation should be put
at the end and some references set to one early module. Which one? Two
choices: NCic or NCicPp (two modules, one with the implementation follows).
Could the same be done for NCicLibrary too in order to bring back the explicit
dependency of NCicEnvironment over NCicLibrary? [ In that case, remember to
change back the exception caught by GrafiteDisambiguate ]
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/ng_kernel/.depend
helm/software/components/ng_kernel/.depend.opt
helm/software/components/ng_kernel/Makefile
helm/software/components/ng_kernel/nCicEnvironment.ml
helm/software/components/ng_kernel/nCicEnvironment.mli
helm/software/components/ng_kernel/nCicLibrary.ml
helm/software/components/ng_kernel/nCicLibrary.mli
helm/software/components/ng_kernel/nCicPp.ml
helm/software/components/ng_kernel/nCicPp.mli