aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| | | | | | | | | | | | | * | | | | [summary] Allow typed projections from global state + rework of internals.Gravatar Emilio Jesus Gallego Arias2017-12-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In the transition towards a less global state handling we have the necessity of mix imperative setting [notably for the modules/section code] and functional handling of state [notably in the STM]. In that scenario, it is very convenient to have typed access to the Coq's `summary`. Thus, I reify the API to support typed access to the `summary`, and implement such access in a couple of convenient places. We also update some internal datatypes to simplify the `frozen` data type. We also remove the use of hashes as it doesn't really make things faster, and most operations are now over `Maps` anyways. I believe this goes in line with recent work by @ppedrot. We also deprecate the non-typed accessors, which were only supposed to be used in the STM, which is now ported to the finer primitives.
| | | | | | | | | | | | | * | | | | [lib] Convenience function for `Dyn.Easy`Gravatar Emilio Jesus Gallego Arias2017-12-09
| | |_|_|_|_|_|_|_|_|_|_|/ / / / / | |/| | | | | | | | | | | | | | |
| | | | | | * | | | | | | | | | | Remove up-to-conversion matching functions.Gravatar Pierre-Marie Pédrot2017-12-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | They were not used anymore since the previous patches.
| | | | | | | | | | | | | * | | | Remove most uses of function extensionality in Program.CombinatorsGravatar Jasper Hugunin2017-12-09
| | |_|_|_|_|_|_|_|_|_|_|/ / / / | |/| | | | | | | | | | | | | |
| | | | | * | | | | | | | | | | [ci] Download ci-sf archives into the proper CI build dir.Gravatar Emilio Jesus Gallego Arias2017-12-09
| |_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Currently, `make ci-sf` downloads and builds the files in the main root directory. we fix that.
| * | | | | | | | | | | | | | 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
|/ / / / / / / / / / / / / /
| | | | | | * / / / / / / / [makefile] Address #6291: install more development files.Gravatar Emilio Jesus Gallego Arias2017-12-08
| |_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As noted in the bug #6291, `.cmx` files are not installed in the coqlib, which yields the warning: ``` Warning 58: no cmx file was found in path for module Sorts, and its interface was not compiled with -opaque ``` We thus install the `cmx` files to fix this problem, and also install the `.o` files for plugins' `.o` to support linking the plugins statically. This closes #5099 and #6291.
| | | * | | | | | | | | | Fix a copy-paste error in ci-ltac2.Gravatar Théo Zimmermann2017-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.
| | | | | * | | | | | | | | | | [ci] CoLoR has moved to githubGravatar Emilio Jesus Gallego Arias2017-12-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Closes #6194 .
* | | | | | | | | | | | | | | | Merge PR #6267: Fix PR merge script.Gravatar Maxime Dénès2017-12-07
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | |
| | | | | * | | | | | | | | | | [default.nix] Add ocpIndent and ocp-index.Gravatar Maxime Dénès2017-12-07
| |_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | |
| | | | | | | * | | | | | | | Getting rid of pf_matches in Hipattern.Gravatar Pierre-Marie Pédrot2017-12-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Funnily enough, the old code is completely bogus. It succeeds in early files of the prelude just because the heterogeneous equality has not been required. This raises an exception which is not the same one as if we tried to rewrite with the identity type first. The only user, the inversion tactic, was actually only relying on Logic.eq and was furthermore not even using the convertibility algorithm. We just perform a syntactic match now.
* | | | | | | | | | | | | | | 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
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | * | | [configure] fix spelling mistakeGravatar Vincent Laporte2017-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
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | * | Additional rewrite lemmas on Ensembles, in Powerset_factsGravatar Joachim Breitner2017-12-06
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | * | | | | | | Getting rid of pf_is_matching in Funind.Gravatar Pierre-Marie Pédrot2017-12-06
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | | | | 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.
| | | | | | | | | | | | | | * | | | | | Overlay for Equations.Gravatar Gaëtan Gilbert2017-12-06
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | * | | Linter: skip PRs older than the linter.Gravatar Gaëtan Gilbert2017-12-06
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * | | | | Fix #6323: stronger restrict universe context vs abstract.Gravatar Gaëtan Gilbert2017-12-06
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In the test we do [let X : Type@{i} := Set in ...] with Set abstracted. The constraint [Set < i] was lost in the abstract. Universes of a monomorphic reference [c] are considered to appear in the term [c].
| | | | | * | | | | | | | | | | | | 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
| |_|_|/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * | | Don't Add LoadPath on CoqIDE startup, #6153Gravatar 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
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | * | [configure] adds a `select_command` functionGravatar Vincent Laporte2017-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
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 13:11:46 +0000