aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* [make] remove unneeded generated file "tolink.ml"Gravatar Emilio Jesus Gallego Arias2017-12-10
| | | | | | | | | | When statically linking plugins, the "DECLARE PLUGIN" macro takes care of properly setting up the loaded module table. This setup was also done by `coqmktop`, thus in order to ease bisecting, we didn't take care of it in the `coqmktop` deprecation. Fixes #6364.
* [build] Remove coqmktop in favor of ocamlfind.Gravatar Emilio Jesus Gallego Arias2017-12-10
| | | | | | | | | | | | | | | | | We remove coqmktop in favor of a couple of simple makefile rules using ocamlfind. In order to do that, we introduce a new top-level file that calls the coqtop main entry. This is very convenient in order to use other builds systems such as `ocamlbuild` or `jbuilder`. An additional consideration is that we must perform a side-effect on init depending on whether we have an OCaml toplevel available [byte] or not. We do that by using two different object files, one for the bytecode version other for the native one, but we may want to review our choice. We also perform some smaller cleanups taking profit from ocamlfind.
* [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
| | | | | New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
* Revert "CI: poc Circleci configuration"Gravatar Arnaud Spiwack2017-12-08
| | | | | | | Committed on master by mistake. Clearly I'm too clumsy to be trusted with push rights. This reverts commit d606a85d53fbd0227b15e18701e2ac4c9d911f34.
* CI: poc Circleci configurationGravatar Arnaud Spiwack2017-12-08
|
* Merge PR #6334: Remove dead code in ReductionopsGravatar Maxime Dénès2017-12-08
|\
* \ Merge PR #6158: Allows a level in the raw and glob printersGravatar Maxime Dénès2017-12-08
|\ \
* \ \ Merge PR #6224: Add alienclean target to remove compilation products with no ↵Gravatar Maxime Dénès2017-12-08
|\ \ \ | | | | | | | | | | | | source.
* \ \ \ Merge PR #6267: Fix PR merge script.Gravatar Maxime Dénès2017-12-07
|\ \ \ \
* \ \ \ \ Merge PR #6290: Rename update to set, Fixes #6196Gravatar Maxime Dénès2017-12-07
|\ \ \ \ \
* \ \ \ \ \ Merge PR #873: New strategy based on open scopes for deciding which notation ↵Gravatar Maxime Dénès2017-12-07
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | to use among several of them
* \ \ \ \ \ \ Merge PR #6142: Single quotes break on WindowsGravatar Maxime Dénès2017-12-07
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6277: Qualified import in coqchkGravatar Maxime Dénès2017-12-07
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6322: Fix #6286 (non stability of micromega csdp cache rebuilding)Gravatar Maxime Dénès2017-12-07
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6321: Use preference for ocamlfind in configureGravatar Maxime Dénès2017-12-07
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6316: Correct typoGravatar Maxime Dénès2017-12-07
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6309: [default.nix] needs ncurses for the test-suiteGravatar Maxime Dénès2017-12-07
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6303: Remove redundant Zcase from the checker.Gravatar Maxime Dénès2017-12-07
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | * Getting rid of the Update constructor in Reductionops.Gravatar Pierre-Marie Pédrot2017-12-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was dead code, probably due to the fact it was once shared with the kernel stack type.
| | | | | | | | | | | | | * Getting rid of the Shift constructor in Reductionops.Gravatar Pierre-Marie Pédrot2017-12-06
| |_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It was actually not used. The only place generating one was easily writable without it.
| | | | | * | | | | | | | Replacing Hashtbl.add by Hashtbl.replace in micromega cache building.Gravatar Hugo Herbelin2017-12-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes #6286 as suggested by PMP. See details of discussion at #6286.
| | | | | | | | | * | | | Rename update to set, fixes #6196Gravatar Paul Steckler2017-12-05
| | | | | | | | | | | | |
| | | | * | | | | | | | | use preference for ocamlfindGravatar Paul Steckler2017-12-05
| |_|_|/ / / / / / / / / |/| | | | | | | | | | |
| | | * | | | | | | | | Correct typoGravatar Martin Vassor2017-12-05
| |_|/ / / / / / / / / |/| | | | | | | | | |
| | * | | | | | | | | [default.nix] explain ncurses dependencyGravatar Vincent Laporte2017-12-05
| | | | | | | | | | |
* | | | | | | | | | | Merge PR #890: Global universe declarationsGravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6266: Safe unmarshalling in the checkerGravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6301: [vernac] Couple of tweaks missing from previous PRs.Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6306: Adding a test for #6304 (a bug with "fix" in notations).Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6300: Clarify operation of sequences, fixes #6095Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6293: Check for Num lib if OCaml >= 4.06, fixes #6162Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6302: Uninstall doc dir, not dev (which is not installed), fixes #6007Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6287: Add merlin to default.nixGravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6210: More complete not-fully-applied error messages, #6145Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | * | | | | | | | [default.nix] needs ncurses for the test-suiteGravatar Vincent Laporte2017-12-04
| |_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | |
| | | | | | | | * | | | | | | | | | | [vernac] Couple of tweaks missing from previous PRs.Gravatar Emilio Jesus Gallego Arias2017-12-04
| |_|_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In particular we must invalidate the state cache in the case of an exception.
| | | | | | | * | | | | | | | | | | Adding a test for #6304 (bug with fix in notations).Gravatar Hugo Herbelin2017-12-03
| |_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | Remove redundant Zcase from the checker.Gravatar Pierre-Marie Pédrot2017-12-02
| |_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was redundant with ZcaseT, the only difference lying in the use or not of fclosures for substerms. This code was removed from the kernel in commit f2f805ed, we finish the work in the checker now.
| | | * | | | | | | | | | | | | uninstall doc dir, not dev (which is not installed), #6007Gravatar Paul Steckler2017-12-01
| |_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | |
| | | * | | | | | | | | | | | check for Num lib if OCaml >= 4.06, #6162Gravatar Paul Steckler2017-12-01
| | | | |_|_|_|_|_|_|/ / / / | | | |/| | | | | | | | | |
| | | | | * | | | | | | | | clarify operation of sequences, #6095Gravatar Paul Steckler2017-12-01
| | | | |/ / / / / / / / / | | | |/| | | | | | | | |
| | | | | | * | | | | | | Update CHANGESGravatar Matthieu Sozeau2017-12-01
| | | | | | | | | | | | |
| | | | | | * | | | | | | Cleanup API for registering universe binders.Gravatar Matthieu Sozeau2017-12-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Regularly declared for for polymorphic constants - Declared globally for monomorphic constants. E.g mono@{i} := Type@{i} is printed as mono@{mono.i} := Type@{mono.i}. There can be a name clash if there's a module and a constant of the same name. It is detected and is an error if the constant is first but is not detected and the name for the constant not registered (??) if the constant comes second. Accept VarRef when registering universe binders Fix two problems found by Gaëtan where binders were not registered properly Simplify API substantially by not passing around a substructure of an already carrier-around structure in interpretation/declaration code of constants and proofs Fix an issue of the stronger restrict universe context + no evd leak This is uncovered by not having an evd leak in interp_definition, and the stronger restrict_universe_context. This patch could be backported to 8.7, it could also be triggered by the previous restrict_context I think.
| | | | | | * | | | | | | [refman] Expand a little on global universes.Gravatar Matthieu Sozeau2017-12-01
| | | | | | | | | | | | |
| | | | | | * | | | | | | Tests for global universe declarationsGravatar Matthieu Sozeau2017-12-01
| | | | | | | | | | | | |
| | | | | | * | | | | | | Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
| |_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced
| | | | | | * | | | | | Documenting the -Q flag of coqchk.Gravatar Pierre-Marie Pédrot2017-12-01
| | | | | | | | | | | |
* | | | | | | | | | | | Merge PR #736: [ci] Test coqchk on the CompCert target.Gravatar Maxime Dénès2017-12-01
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6256: CI: better ocaml warning checksGravatar Maxime Dénès2017-12-01
|\ \ \ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 14:12:36 +0000