| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-26 | Fix ocamldebug-coq for packed gramlib | Gaëtan Gilbert | |
| 2018-11-24 | Merge PR #8933: Make initial evar map argument to check_evars_are_solved ↵ | Pierre-Marie Pédrot | |
| optional. | |||
| 2018-11-24 | Apply suggestions from code review | Théo Zimmermann | |
| Thanks to @Zimmi48 as always for the careful review. Co-Authored-By: ejgallego <e+git@x80.org> | |||
| 2018-11-24 | [ci] [doc] Note about `overlay-maintainers` team. | Emilio Jesus Gallego Arias | |
| 2018-11-24 | [ci] [doc] Note about `create-overlays.sh` | Emilio Jesus Gallego Arias | |
| 2018-11-24 | [ci] [doc] Split user/developer README, add info about Nix/Docker CI | Emilio Jesus Gallego Arias | |
| 2018-11-23 | Merge PR #9055: [dev] fix create_overlay wrt branch names containing / | Emilio Jesus Gallego Arias | |
| 2018-11-23 | Merge PR #9044: Remove pidetop from CI | Emilio Jesus Gallego Arias | |
| 2018-11-23 | Adding overlay. | Pierre-Marie Pédrot | |
| 2018-11-23 | Merge PR #9021: merge-pr: Improve overlay check | Maxime Dénès | |
| 2018-11-22 | [dev] fix create_overlay wrt branch names containing / | Enrico Tassi | |
| 2018-11-21 | Remove pidetop from CI | Maxime Dénès | |
| pidetop relies on some rather low level API from STM, which we'd like to change. It does not seem maintained much anymore, and still hasn't moved to github. | |||
| 2018-11-21 | [camlp5] Remove dependency on camlp5. | Emilio Jesus Gallego Arias | |
| 2018-11-21 | Merge PR #8985: [gramlib] [build] Switch make-based system to packed gramlib | Enrico Tassi | |
| 2018-11-21 | Add overlay for solve-remaining-evars-initial-arg | Gaëtan Gilbert | |
| 2018-11-21 | Merge PR #8961: dune: link kernel in checker instead of copying files | Pierre-Marie Pédrot | |
| 2018-11-21 | [legacy proof engine] Remove some cruft. | Emilio Jesus Gallego Arias | |
| We remove the `Proof_types` file which was a trivial stub, we also cleanup a few layers of aliases. This is not a lot but every little step helps. | |||
| 2018-11-21 | [gramlib] [build] Switch make-based system to packed gramlib | Emilio Jesus Gallego Arias | |
| This makes the make-based build system stop linking to Camlp5's gramlib and instead links to our own gramlib. We use the style done in the packing of `Stdlib` in OCaml 4.07. As to introduce a minimal amount of noise in history we use an autogenerated `gramlib__pack` directory. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2018-11-20 | Merge PR #8948: [dune] Some tweaks to docs. | Théo Zimmermann | |
| 2018-11-20 | [dune] Only build printers when the ltac plugin is available. | Emilio Jesus Gallego Arias | |
| This fixes a problem reported by @Zimmi48 in #8948, IMHO we should be able to have a clean build of core Coq. | |||
| 2018-11-20 | gitlab: Install stdlib doc in build:base | Gaëtan Gilbert | |
| Looks like we forgot to adapt this when we split off the sphinx job and stopped using -with-doc yes. | |||
| 2018-11-20 | Fix dune-dbg using checker/main -> checker/coqchk | Gaëtan Gilbert | |
| 2018-11-20 | Merge PR #7925: Clean transparent state | Maxime Dénès | |
| 2018-11-19 | Merge PR #9003: [vernacextend] Consolidate extension points API | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #8902: [ltac] Use CAst nodes in the tactic AST. | Pierre-Marie Pédrot | |
| 2018-11-19 | Adding overlays. | Pierre-Marie Pédrot | |
| 2018-11-19 | Rename TranspState into TransparentState. | Pierre-Marie Pédrot | |
| 2018-11-19 | Proper record type and accessors for transparent states. | Pierre-Marie Pédrot | |
| This is documented in dev/doc/changes.md. | |||
| 2018-11-19 | Move transparent_state to its own module. | Pierre-Marie Pédrot | |
| 2018-11-18 | merge-pr: Improve overlay check | Gaëtan Gilbert | |
| 2018-11-18 | Merge PR #9018: [devtools] Small script to setup overlays automatically | Gaëtan Gilbert | |
| 2018-11-17 | [devtools] Small script to setup overlays automatically | Emilio Jesus Gallego Arias | |
| This is very preliminary but you should get the idea. The script tries to build contribs, then creates a branch and sets the remote properly as to submit a PR. Usage example: ``` ./dev/tools/create_overlays.sh ejgallego 9999 ltac2 elpi ``` This only works for contributions hosted in github for now. | |||
| 2018-11-17 | [vernacextend] Consolidate extension points API | Emilio Jesus Gallego Arias | |
| We group the extension API and datatypes under `Vernacextend`. This means that the base plugin dependency is now `coq.vernac` from `coq.stm`. This is quite important as for example the LSP server won't like to link the STM in. LTAC still depends on the STM by means of the ltac_profile part tho. The next step could be to move the extension point below `Vernacexpr`. | |||
| 2018-11-17 | [ci] Uniformize casing of makefile targets and ci variables. | Emilio Jesus Gallego Arias | |
| This is convenient as to have better automation. | |||
| 2018-11-17 | [ci] Cleanup of old overlays. | Emilio Jesus Gallego Arias | |
| 2018-11-17 | [CoqProject] Abstract warning function for CoqProject readers. | Emilio Jesus Gallego Arias | |
| `CoqProject_file` uses the feedback system, however this is not very convenient in some scenarios such as `coqdep` that has to be run very early in the build process [and thus in "boot" mode]. We thus make the warning function a paramater. Should fix #8913. | |||
| 2018-11-17 | [ltac] Use CAst nodes in the tactic AST. | Emilio Jesus Gallego Arias | |
| This provides several advantages to people serializing tactic scripts. Appearance of the involved constructors is common enough as to bother to submit this PR. | |||
| 2018-11-16 | Remove the implicit tactic feature following #7229. | Pierre-Marie Pédrot | |
| 2018-11-13 | Merge PR #8976: CoqHammer CI | Gaëtan Gilbert | |
| 2018-11-13 | [vernac] Rename Vernacinterp to Vernacextend and move extension functions there. | Emilio Jesus Gallego Arias | |
| This PR fixes an issues that was bugging me for some time, namely that `Vernacinterp` really means `Vernacextend`. We thus rename the file and move the associated functions there, which were incorrectly placed in `Vernacentries`. Note the beneficial effects on reducing the `.mli` API. | |||
| 2018-11-13 | Merge PR #8978: nix helpers for debugging external projects from CI | Emilio Jesus Gallego Arias | |
| 2018-11-12 | Skip submodules in HoTT CI script. | Gaëtan Gilbert | |
| Avoid downloading Coq. | |||
| 2018-11-12 | CoqHammer CI | Lukasz Czajka | |
| 2018-11-12 | Helpers for debugging external projects from CI | Vincent Laporte | |
| 2018-11-10 | [ci] Add paramcoq to CI. | Emilio Jesus Gallego Arias | |
| 2018-11-09 | Merge PR #8949: Remove checker printers | Emilio Jesus Gallego Arias | |
| 2018-11-09 | Adding an overlay for #8601. | Pierre-Marie Pédrot | |
| 2018-11-08 | [dune] Some tweaks to docs. | Emilio Jesus Gallego Arias | |
| 2018-11-08 | Remove checker printers | Gaëtan Gilbert | |
| Now that the checker is using the regular kernel files it can also use the normal printers. | |||
| 2018-11-08 | Merge PR #8944: Revert PR #8923 (require camlp5 >=7.06) | Gaëtan Gilbert | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |