Rodolphe Lepigre

I'm not particularly fond of that behavior in Coq, what is wrong with adding a `require open ` in file `C`?

Well, that is not useful because Lambdapi itself does that work. If an object file is outdated, it is automatically rebuilt. That has always been the case, since the beginning...

That being said, a `lambadpi depend` command could be useful at some point. However this is not easy to implement: analysing the dependencies of a file currently require parsing it,...

For your `Makefile` you should take the same approach as with `dune` in OCaml, the management of dependencies is managed by `lambdapi`, not the `Makefile` This means that your target...

If you send me a tarball with the files of your repository I can have a look. I will also document that, and maybe provide a command `lambdapi init `...

OK, I'm looking into it.

OK, the behaviour after ea02f8a519dd8864c8da1a2a88e5c5e3d7065490 is the expected one now. There was an issue when compiling several different files at once. I also made it so that compilation is not...

> Should I change my Makefile? No, I did it for you. > But aren't you going to recompile everything, even the files that do not need to be recompiled?...

Yes, this is not a desirable "feature" at all, as I have said numerous times. The problem is, we can't fix it in Lambdapi if it is not fixed in...

Well, I don't know a single other language with that behavior. In OCaml for example, you cannot use `M.f` inside the definition of the module `M` itself. I don't remember...