Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | | | | * | make-both-single-timing-files: fix --sort-by=diff | 2018-07-07 | ||
| |_|_|_|_|_|/ |/| | | | | | | ||||
| | * | | | | | Output UTF-8 explicitly in timing tools | 2018-07-07 | ||
| | | | | | | | ||||
* | | | | | | | Merge PR #7921: Archive the `gallina` tool | 2018-07-07 | ||
|\ \ \ \ \ \ \ | ||||
| | | | | | | * | Add an overlay. | 2018-07-07 | ||
| | | | | | | | | ||||
* | | | | | | | | Merge PR #7956: Rebuild coqtop$(EXE) in "make coqbinaries" in addition to ↵ | 2018-07-07 | ||
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | coqtop.opt$(EXE). | |||
| | | | | | | | * | Introduce a Pcoq.Entry module for functions that ought to be exported. | 2018-07-07 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We deprecate the corresponding functions in Pcoq.Gram. The motivation is that the Gram module is used as an argument to Camlp5 functors, so that it is not stable by extension. Enforcing that its type is literally the one Camlp5 expects ensures robustness to extension statically. Some really internal functions have been bluntly removed. It is unlikely that they are used by external plugins. | |||
| | | | | | | | * | Remove dead code that used to be there for CamlpX compatibility. | 2018-07-07 | ||
| |_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Part of this code has been introduced very recently in 7c62654 in spite of the existence of a proper API. This means that this should be better documented. | |||
* | | | | | | | | Merge PR #8005: Fix compilation of Coq with camlp5 master branch. | 2018-07-07 | ||
|\ \ \ \ \ \ \ \ | |_|_|_|/ / / / |/| | | | | | | | ||||
* | | | | | | | | Merge PR #8001: Cache the build of the Nix package using Cachix. | 2018-07-06 | ||
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR #7821: [refine] obey the use_unification_heuristics flag | 2018-07-06 | ||
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR #8008: Add test for #8004. | 2018-07-06 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
| | | * | | | | | | | | [pkg:nix] Add more comments and allow overriding extra substituters. | 2018-07-06 | ||
| | | | | | | | | | | | ||||
| * | | | | | | | | | | Add test for #8004. | 2018-07-06 | ||
|/ / / / / / / / / / | ||||
| | | * / / / / / / | Fix compilation of Coq with camlp5 master branch. | 2018-07-06 | ||
| |_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There was a conflict in the name of an exported function. A good argument in favour of PR #7898. | |||
* | | | | | | | | | Merge PR #7990: Convert timing tool to python3 | 2018-07-05 | ||
|\ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | refine: obey the use_unification_heuristics flag | 2018-07-05 | ||
| |/ / / / / / / / |/| | | | | | | | | ||||
* | | | | | | | | | Merge PR #7991: Make Travis faster by removing more builds. | 2018-07-05 | ||
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR #7994: Make bin/ in makefile, not configure. | 2018-07-05 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
| | | | * | | | | | | | [pkg:nix] Stop using lib.inNixShell. | 2018-07-05 | ||
| | | | | | | | | | | | ||||
| | | | * | | | | | | | [pkg:nix] Change the download method. | 2018-07-05 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This will allow for better reuse of the cache when the URL is different but the archive is the same. | |||
| | | | * | | | | | | | [pkg:nix] Pass through the ocamlPackages version used to build. | 2018-07-05 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This will be useful for users wanting to build a plugin using this package. | |||
| | | | * | | | | | | | [pkg:nix] Cache the build using Cachix when signing key is set. | 2018-07-05 | ||
| |_|_|/ / / / / / / |/| | | | | | | | | | ||||
| | * | | | | | | | | Remove some Travis jobs to make the build faster. | 2018-07-05 | ||
| |/ / / / / / / / |/| | | | | | | | | ||||
| | | | | | | | * | Turn a dead branch into an assertion failure in VM reification. | 2018-07-05 | ||
| |_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In #7607, dead code that used to handle non-dependent return predicates was removed. This made the reification branch expecting non-functions in predicates dead code. We fix this by using an assert instead. | |||
* | | | | | | | | Merge PR #7746: Many small cleanups removing unused arguments and functions | 2018-07-05 | ||
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR #7979: TACTIC EXTEND in coqpp | 2018-07-05 | ||
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR #7973: Add a test build on NixOS to GitLab CI. | 2018-07-04 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #7989: [ci] Avoid annoying detached head warning. | 2018-07-04 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | * | | | | | | Convert timing tools to run with both python2 and python3 | 2018-07-04 | ||
| | | | | | | | | | | | | ||||
* | | | | | | | | | | | | Merge PR #7993: doc: Fix markup in Calculus of Inductive Constructions | 2018-07-04 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | * | | | Remove letouzey from CODEOWNERS since he left the Coq organization. | 2018-07-04 | ||
| | | | | | | | |_|/ / / | | | | | | | |/| | | | | ||||
| * | | | | | / | | | | | doc: Fix markup in Calculus of Inductive Constructions | 2018-07-04 | ||
| | |_|_|_|_|/ / / / / | |/| | | | | | | | | | ||||
* | | | | | | | | | | | Merge PR #7992: Print something after the build completed if it wasn't a ↵ | 2018-07-04 | ||
|\ \ \ \ \ \ \ \ \ \ \ | |/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | runner failure. | |||
| * | | | | | | | | | | Print something after the build completed if it wasn't a runner failure. | 2018-07-04 | ||
|/ / / / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This can then be leveraged by @coqbot to know which builds to restart. | |||
| * / / / / / / / / | [ci] Avoid annoying detached head warning. | 2018-07-04 | ||
|/ / / / / / / / / | ||||
| | | | * / / / / | Make bin/ in makefile, not configure. | 2018-07-04 | ||
| |_|_|/ / / / / |/| | | | | | | | ||||
| * | | | | | | | Add a shell.nix that is not pinned to satisfy some developers' preference. | 2018-07-03 | ||
| | | | | | | | | ||||
| * | | | | | | | Refactor default.nix to use optionals. | 2018-07-03 | ||
| | | | | | | | | ||||
| * | | | | | | | Fix timing tools on NixOS. | 2018-07-03 | ||
| | | | | | | | | ||||
| | | | | | | * | [test suite] Test case for attributes | 2018-07-03 | ||
| | | | | | | | | ||||
| | | | | | | * | Document attributes. | 2018-07-03 | ||
| | | | | | | | | ||||
| | | | | | | * | fix syntax of .mlg | 2018-07-03 | ||
| | | | | | | | | ||||
| | | | | | | * | Describe attributes in the documentation. | 2018-07-03 | ||
| | | | | | | | | ||||
| | | | | | | * | [vernac] use a record for the contents of the “deprecated” attribute | 2018-07-03 | ||
| | | | | | | | | ||||
| | | | | | | * | [vernac] use plain strings as attribute names | 2018-07-03 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The concrete syntax is still restricted to identifiers. | |||
| | | | | | | * | [vernac] indentation | 2018-07-03 | ||
| | | | | | | | | ||||
| | | | | | | * | [vernac] Generic syntax for flags/attributes | 2018-07-03 | ||
| | | | | | | | | ||||
| | | | | | | * | [vernac] Generic parsing rules for attributes | 2018-07-03 | ||
| | | | | | | | | ||||
| | | | | | | * | [vernac] Add a “deprecated” attribute | 2018-07-03 | ||
| | | | | | | | | ||||
| | | | | | | * | Allow “Let”-defined coercions | 2018-07-03 | ||
| | | | | | | | |