| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
#2168)
We replace Global.lookup_constant by our own code that looks for a module
and enters its implementation. This is still preliminary work, I would prefer
to understand more completely the part about module substitutions when
entering an applied functor. But this code already appears to work quite well.
Anyway, since we only search for constants, we don't need to reconstitute a
100% accurate environment, as long as the same objects are in it.
Note:
- Digging inside module structures is slower than just using
Global.lookup_constant. Hence we try to avoid it as long as we could.
Only in front of axioms (or in front of constant unknown to Global)
do we check whether we have an inner-module implementation for this
constant. There is some memoization of the search for internal
structure_body out of a module_path.
- In case of inner-module axioms, we might not be able to print
its type, but only its long name.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14600 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
* generalize the use of .mllib to build all cma, not only in plugins/
* the .mllib in plugins/ now mention Bruno's new _mod.ml files
* lots of .cmo enumerations in Makefile.common are removed, since
they are now in .mllib
* the list of .cmo/.cmi can be retreive via a shell script line,
see for instance rule install-library
* Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not
_files_
* a -I option to coqdep_boot allows to control piority of includes
(some files with the same names in kernel and checker ...)
This is quite a lot of changes, you know who to blame / report to
if something breaks.
... and last but not least I've started playing with ocamlbuild.
The myocamlbuild.ml is far from complete now, but it already allows
to build coqtop.{opt,byte} here. See comments at the top of
myocamlbuild.ml, and don't hesitate to contribute, either for completing
or simplifying it !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
letouzey