| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
implementation from Detyping.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
With a minimal diff (so I'm not putting quotes ` ` around all the code).
|
|
|
|
|
|
This is a temporary workaround, until we fix the underlying issue which
makes coqtop hang on those tests.
|
|
|
|
The code generating the projection was unconditionally generating
pattern-matchings, although this is incorrect for primitive records.
|
|
|
|
|
|
|
|
|
|
|
|
restructuration
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
CAMLPKGS is now used to hold extra findlib -packages
The previous solution was to use CAMLFLAGS but since 4.05 an
invocation of `ocamlopt -pack useless.cmxa foo.cmx -o packedfoo.cmx`
fails saying that `useless.cmxa` is not a compilation unit description.
CAMLPKGS is used in all `ocamlopt` invocations but for the one
performing the packing.
|
|
The build chain is always
ml -> cmo -> cma
ml -> cmx -> cmxa -> cmxs
If we are packing, then it becomes
ml -> cmo \
ml -> cmo --> cmo -> cma
ml -> cmo /
ml -> cmxo \
ml -> cmxo --> cmxo -> cmxa -> cmxs
ml -> cmxo /
The interest of always having a .cma or .cmxa is that such file can
carry linking flags, that in findlib terms means which
-package was use to build the plugin.
|
|
|
|
coq-makefile's tests do depend on this
|
|
|
|
Deployment doesn't work on PRs, so I have to push it directly, sorry for
the noise.
|
|
|
