Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Rename the "chan" argument into "fmt" in coqpp_main. | 2018-07-02 | |
| | |||
* | Remove the hardcoded compatibility wit_hyp -> wit_var from the parser. | 2018-07-02 | |
| | |||
* | Slight simplification of the Tacentries API to register ML tactics. | 2018-07-02 | |
| | | | | It was forcing the macro to generate code that was useless. | ||
* | Documenting the syntax changes. | 2018-07-02 | |
| | |||
* | Moving various ml4 files to mlg. | 2018-07-02 | |
| | |||
* | Implementing TACTIC EXTEND in coqpp. | 2018-07-02 | |
| | |||
* | Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵ | 2018-07-02 | |
|\ | | | | | | | points of Camlp5 | ||
* \ | Merge PR #7961: [api] Fix wrong deprecation warning (#7915) | 2018-07-02 | |
|\ \ | |||
| * | | [api] Fix wrong deprecation warning (#7915) | 2018-07-01 | |
|/ / | | | | | | | | | | | | | Fixes: #7915. Due to a change in the original misctypes removal PR, the deprecation notice went out of sync. | ||
* | | Merge PR #7964: Document that GITURL variables shouldn't have a trailing ↵ | 2018-07-01 | |
|\ \ | | | | | | | | | | .git anymore. | ||
* \ \ | Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, ↵ | 2018-07-01 | |
|\ \ \ | | | | | | | | | | | | | Z into three files | ||
* \ \ \ | Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation ↵ | 2018-07-01 | |
|\ \ \ \ | | | | | | | | | | | | | | | | format). | ||
* \ \ \ \ | Merge PR #7759: Workaround to fix #7731 (printing not splitting line at ↵ | 2018-07-01 | |
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | break hint). | ||
* \ \ \ \ \ | Merge PR #7960: [build] Remove target binary before copy. | 2018-06-30 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #7949: Split the Ssrmatching module between code and grammar rules. | 2018-06-30 | |
|\ \ \ \ \ \ \ | |||
| * | | | | | | | Split the Ssrmatching module between code and grammar rules. | 2018-06-30 | |
|/ / / / / / / | | | | | | | | | | | | | | | | | | | | | | Fixes #7857. | ||
| | | | | | * | Adding an overlay for the PR. | 2018-06-29 | |
| | | | | | | | |||
| | | | | | * | Documenting the transition strategy of GEXTEND. | 2018-06-29 | |
| | | | | | | | |||
| | | | | | * | Port g_tactic to the homebrew GEXTEND parser. | 2018-06-29 | |
| | | | | | | | |||
| | | | | | * | Port g_toplevel to the homebrew GEXTEND parser. | 2018-06-29 | |
| | | | | | | | |||
| | | | | | * | Port g_vernac to the homebrew GEXTEND parser. | 2018-06-29 | |
| | | | | | | | |||
| | | | | | * | Port g_proofs to the homebrew GEXTEND parser. | 2018-06-29 | |
| | | | | | | | |||
| | | | | | * | Port g_constr to the homebrew GEXTEND parser. | 2018-06-29 | |
| | | | | | | | |||
| | | | | | * | Port g_prim to the homebrew GEXTEND parser. | 2018-06-29 | |
| | | | | | | | |||
| | | | | | * | Use a homebrew parser to replace the GEXTEND extension points of Camlp5. | 2018-06-29 | |
| |_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The parser is stupid and the syntax is almost the same as the previous one. The only difference is that one needs to wrap OCaml code between { braces } so that quoting works out of the box. Files requiring such a syntax are handled specifically by the type system and need to have a .mlg extension instead of a .ml4 one. | ||
| | | | | * | Document that GITURL variables shouldn't have a trailing .git anymore. | 2018-06-29 | |
| |_|_|_|/ |/| | | | | | | | | | | | | | | This allows to append /archive at the end. | ||
* | | | | | Merge PR #7918: Mini-update of version history with recent changes. | 2018-06-29 | |
|\ \ \ \ \ | |||
| | | | | * | Splitting primitive numeral parser/printer for positive, N, Z into three files. | 2018-06-29 | |
| | | | | | | |||
| | | * | | | Workaround to fix #7731 (printing not splitting line at break hint). | 2018-06-29 | |
| | | | |/ | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In some cases, Format's inner boxes inside an outer box act as break hints, even though there are already "better" break hints in the outer box. We work around this "feature" by not inserting a box around the default printing rule for a notation if there is no effective break points in the box. See https://caml.inria.fr/mantis/view.php?id=7804 for the related OCaml discussion. | ||
| | | | * | Fixes #7712 (an anomaly in reporting bad recursive notation format). | 2018-06-29 | |
| | | |/ | |||
* | | | | Merge PR #7080: Swapping Context and Constr and defining declarations on ↵ | 2018-06-29 | |
|\ \ \ \ | | | | | | | | | | | | | | | | constr in Constr | ||
| | | * | | [build] Remove target binary before copy. | 2018-06-29 | |
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | Fixes #7666. Due to shared mapping of executables Linux doesn't allow to overwrite binaries that are running; we do as `ocamlopt` and delete the target file before copy. | ||
* | | | | Merge PR #7890: Inline a function from Quote used in setoid_ring. | 2018-06-29 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #7745: Make type Environ.globals abstract + simplify ↵ | 2018-06-29 | |
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | Environ.retroknowledge | ||
* \ \ \ \ \ | Merge PR #7950: Documentation for 8.8.1 | 2018-06-29 | |
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | | | |||
* | | | | | | Merge PR #7860: Fix #7704: Launching coqide through PATH fails. | 2018-06-28 | |
|\ \ \ \ \ \ | |||
| | * | | | | | CHANGES for 8.8.1. | 2018-06-28 | |
| | | | | | | | |||
| | * | | | | | Self-credit for the work done. | 2018-06-28 | |
| |/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I reused the sentence from the version 8.7 credits. It wasn't initially decided like this but it looks like I'm the de facto maintainer for this release as well. | ||
* | | | | | | Merge PR #7948: Syntax for naming an existential variable | 2018-06-28 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #7928: Fix 'unbound variable' issue on Windows packaging jobs. | 2018-06-28 | |
|\ \ \ \ \ \ \ | |||
| | * | | | | | | wrong sphinx syntax | 2018-06-28 | |
| | | | | | | | | |||
* | | | | | | | | Merge PR #7946: Update maintainers for native/VM files in pretyping | 2018-06-28 | |
|\ \ \ \ \ \ \ \ | |||
| | | * | | | | | | Update gallina-extensions.rst | 2018-06-28 | |
| |_|/ / / / / / |/| | | | | | | | | | | | | | | | I knew this feature existed but I did not remember the syntax and I could not find it in the manual | ||
* | | | | | | | | Merge PR #7937: Mention Consortium in README | 2018-06-28 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #7917: Critical bugs: added #3243 and Gonthier's bug in lazy machine. | 2018-06-28 | |
|\ \ \ \ \ \ \ \ \ | |||
| | | | | | * | | | | Deprecate Environ.retroknowledge function in favor of the projection | 2018-06-28 | |
| | | | | | | | | | | |||
| | | | | | * | | | | [env.env_rel_context.env_rel_ctx] -> [rel_context env] | 2018-06-28 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It's a bit shorter and more direct. | ||
| | | | | | * | | | | Make Environ.globals abstract. | 2018-06-28 | |
| |_|_|_|_|/ / / / |/| | | | | | | | | |||
* | | | | | | | | | Merge PR #7932: CoqIDE scrolls the proof buffer down to the first goal. | 2018-06-28 | |
|\ \ \ \ \ \ \ \ \ | |||
| | | | * | | | | | | Update maintainers for native/VM files in pretyping | 2018-06-28 | |
| |_|_|/ / / / / / |/| | | | | | | | |