| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The structure of the Context module was refined in such a way that:
- Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module.
- Types and functions related to rel-context were put into the Context.Rel module.
- Types and functions related to named-context declarations were put into the Context.Named.Declaration module.
- Types and functions related to named-context were put into the Context.Named module.
- Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module.
- Types and functions related to named-list-context were put into Context.NamedList module.
Some missing comments were added to the *.mli file.
The output of ocamldoc was checked whether it looks in a reasonable way.
"TODO: cleanup" was removed
The order in which are exported functions listed in the *.mli file was changed.
(as in a mature modules, this order usually is not random)
The order of exported functions in Context.{Rel,Named} modules is now consistent.
(as there is no special reason why that order should be different)
The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file.
(as there is no special reason to define them in a different order)
The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do.
(Now they are called Context.{Rel,Named}.fold_{inside,outside})
The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated.
Thrown exceptions are now documented.
Naming of formal parameters was made more consistent across different functions.
Comments of similar functions in different modules are now consistent.
Comments from *.mli files were copied to *.ml file.
(We need that information in *.mli files because that is were ocamldoc needs it.
It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function,
we can see the comments also there and do not need to open a different file if we want to see it.)
When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1.
(UTF-8 characters are used in our ocamldoc markup)
"open Context" was removed from all *.mli and *.ml files.
(Originally, it was OK to do that. Now it is not.)
An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
|
| |\ \ \
| |/ /
|/| /
| |/
| | |
Conflicts:
lib/cSig.mli
|
| | |
| |
| |
| |
| | |
Linking a module twice is unsafe and warning 31 will be fatal by default in
OCaml 4.03. See PR#5461.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
CString was linked after Serialize, although the later was using CString.equal.
This had not been noticed so far because OCaml was ignoring functions marked as
external in interfaces (which is the case of CString.equal) when considering
link dependencies. This was changed on the OCaml side as part of the fix of
PR#6956, so linking was now failing in several places.
|
| |\| |
|
| | |
| |
| |
| | |
"dev/printers.cma" to be loadable within "ocamldebug".
|
| | | |
|
| | |
| |
| |
| | |
characters.
|
| |\| |
|
| | | |
|
| |\| |
|
| |\ \ |
|
| | |/ |
|
| | | |
|
| |\| |
|
| | | |
|
| | |
| |
| |
| | |
If it was intentional, please commit again separately.
|
| | |
| |
| |
| |
| | |
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
|
| |\| |
|
| | |
| |
| |
| |
| | |
The target creation process should eventually be automated, because it
is tedious and error-prone as witnessed by this commit.
|
| | |
| |
| |
| | |
(48d611ff2a).
|
| |\| |
|
| | |
| |
| |
| | |
On Fedora, `which 2>&1 >/dev/null` doesn't silence stderr, while `which >/dev/null 2>&1` does.
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
Calling md5sum test earlier, at the time coqchk is built, rather than
at testing time, hopefully moving it closer to what it is supposed to
occur.
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
Broke the build.
This reverts commit ef6459b00999a29183edc09de9035795ff7912e9.
|
| |\| |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
May still be wrong on Windows, though.
|
| | |
| |
| |
| |
| | |
Nothing is done for camlp4
There is an issue with computing camlbindir
|
| |\|
| |
| |
| |
| |
| |
| | |
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.
Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.
If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.
Failure to precompile is a hard error, since it is now explicitly required
by the user.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
Btw, also unset the READABLE_ML4 option, which probably caused
this issue. No, we normally do *not* want to see the internals
of .ml generated out of a .ml4 (except during some specific debug
sessions). It is *so* easy otherwise to edit the wrong .ml by
mistake and forget to edit the original .ml4.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
together with the tactic monad.
The move is not complete yet, because some file candidates for this directory
have almost useless dependencies in other ones that should not be moved.
|
| | | |
|
| |/
|
|
|
| |
3.12.1, ocamldep was able to deal with .ml4, so that building .mllib.d
is the only feature that coqdep_boot was still required for).
|
| | |
|
| |
|
|
|
|
| |
(Sorry, was not intended to be pushed)
This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
|
| |
|
|
|
|
|
| |
In particular:
- abstracting the code using calls to Unix opendir, stat, and closedir,
- uniformly using warnings when a directory does not exist (coqtop was
ignoring silently and coqdep was exiting via handle_unix_error).
|
| |
|
|
| |
So you can link a coqtop compiled (by opam) without coqide to a stand alone coqide (binary distributed)
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
have x permission"
This reverts commit 607503b28fca50f4b76b2237d5ca13802b8252fa.
|
Matej Kosik
Guillaume Melquiond
Maxime Dénès
Pierre-Marie Pédrot
Hugo Herbelin
Matthieu Sozeau
Matthieu Sozeau
Jason Gross
Pierre Boutillier
Pierre Letouzey
Enrico Tassi
Pierre Boutillier