| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-12-09 | [doc] Enable Warning 50 [incorrect doc comment] and fix comments. | Emilio Jesus Gallego Arias | |
| This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :) | |||
| 2018-12-05 | Merge PR #9065: [gramlib] Remove `Ploc.t` in favor of `Loc.t` | Pierre-Marie Pédrot | |
| 2018-11-30 | [vernac] [hooks] Refactor towards optional hooks. | Emilio Jesus Gallego Arias | |
| We make `declaration_hook`s optional arguments everywhere, and thus we avoid some "fake" functions having to be passed. This identifies positively the code really using hooks [funind, rewrite, coercions, program, and canonicals] and helps moving toward some hope of reification. | |||
| 2018-11-30 | [gramlib] Remove `Ploc.t` in favor of `Loc.t` | Emilio Jesus Gallego Arias | |
| The types are identical and we have no more reason for the split. Note the following TODOS: - discrepancy of `Ploc.after` with `CLexer.after` - discrepancy of `Ploc.comments` with `CLexer.comments` - `Ploc.dummy` vs `Loc.t option` | |||
| 2018-11-28 | [ltac] Remove aliases already present in the lower layers. | Emilio Jesus Gallego Arias | |
| We remove a few aliases present in the lower layers [`Genintern/Tactypes`] from `Tacexpr`. IMHO this enlarges the API for no good purpose, and difficults analysis. | |||
| 2018-11-27 | Merge PR #8850: Private universes for opaque polymorphic constants. | Matthieu Sozeau | |
| 2018-11-24 | Merge PR #8933: Make initial evar map argument to check_evars_are_solved ↵ | Pierre-Marie Pédrot | |
| optional. | |||
| 2018-11-23 | Adding overlay. | Pierre-Marie Pédrot | |
| 2018-11-23 | Overlay for private polymorphic universes | Gaëtan Gilbert | |
| 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 | [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 #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-18 | Merge PR #9018: [devtools] Small script to setup overlays automatically | Gaëtan Gilbert | |
| 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] 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-09 | Adding an overlay for #8601. | Pierre-Marie Pédrot | |
| 2018-11-06 | Add overlay for Equations | Matthieu Sozeau | |
| 2018-11-05 | Merge PR #8515: Command driven attributes | Pierre-Marie Pédrot | |
| 2018-11-03 | Merge PR #8844: Move abstract out of tactics.ml | Pierre-Marie Pédrot | |
| 2018-11-02 | Add overlays (command driven attributes) | Gaëtan Gilbert | |
| 2018-10-31 | Merge PR #8688: Generalizing the various evar_map printers in Termops over ↵ | Pierre-Marie Pédrot | |
| an environment | |||
| 2018-10-30 | Merge PR #8750: [ci] [doc] Notes about branch names. | Gaëtan Gilbert | |
| 2018-10-30 | Overlays (#8844 split-tactics) | Gaëtan Gilbert | |
| 2018-10-30 | Adding overlay for coq-elpi | Hugo Herbelin | |
| 2018-10-26 | Fix overlay for this extension of the PR. To be removed. | Matthieu Sozeau | |
| 2018-10-26 | PR 8671: Add overlay for plugin-tutorial | Matthieu Sozeau | |
| 2018-10-26 | Overlay for kernel entries change | Maxime Dénès | |
| 2018-10-17 | [ci] [doc] Notes about branch names. | Emilio Jesus Gallego Arias | |
| I'd like to add this convention as it is very convenient for the development of dev tools. Example, I can do `setup-coq-devs ltac equations` and then get a fully composed tree. Similarly for preparing overlays. | |||
| 2018-10-11 | [vernac] Remove unused abstraction from declaration_hook type. | Emilio Jesus Gallego Arias | |
| "Declaration" hooks can be polymorphic on their return type, however this facility doesn't seem used in the codebase. We thus remove the polymorphism with the hope to be able to reify the control later on. | |||
| 2018-10-08 | Merge PR #8554: Fixes #8553: regression of tactic "change" under binders. | Pierre-Marie Pédrot | |
| 2018-10-05 | [kernel] Remove section paths from `KerName.t` | Maxime Dénès | |
| We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code. Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not. | |||
| 2018-10-02 | [ci] overlay for elpi | Enrico Tassi | |
| 2018-09-27 | Overlays for Ltac2 and Equations. | Hugo Herbelin | |
| 2018-09-25 | overlay to test elpi 1.1 | Enrico Tassi | |
| 2018-09-15 | Overlay for cross-crypto. | Hugo Herbelin | |
| 2018-09-10 | Ltac2 overlay. | Hugo Herbelin | |
| 2018-09-03 | Merge PR #8064: Numeral notation (revisited again) | Hugo Herbelin | |
| 2018-09-03 | Merge PR #7085: Turn the kernel reduction sharing flag into an argument ↵ | Maxime Dénès | |
| passed in the cache | |||
| 2018-09-01 | Add overlay for HoTT | Jason Gross | |
| The overlay for HoTT should be merged right after this PR. | |||
| 2018-08-31 | Download tarball instead of cloning external projects (when $CI is set). | Théo Zimmermann | |
| This allows to use fixed commits and not just branches or tags. We keep using git clone when $FORCE_GIT is set (for projects on gforge.inria.fr and projects pulling dependencies through git submodules). fiat-parsers also calls git submodule, but inside its own Makefile. | |||
| 2018-07-26 | Adding an overlay for Mtac2. | Pierre-Marie Pédrot | |
| 2018-07-25 | Add overlay for Equations | Gaëtan Gilbert | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |