| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | 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 | |
| 2018-07-25 | Merge PR #8063: Direct implementation of Ascii.eqb and String.eqb (take 2) | Hugo Herbelin | |
| 2018-07-24 | Add overlay for Equations. | Gaëtan Gilbert | |
| 2018-07-17 | Add overlay for Coq-Equations for QuestionMark. | Siddharth Bhat | |
| The changed QuestionMark structure breaks Coq-Equations. Add an overlay to fix this. | |||
| 2018-07-16 | Add overlay for QuickChick | Jason Gross | |
| 2018-07-12 | Clean-up user-overlays folder. | Théo Zimmermann | |
| 2018-07-07 | Add an overlay. | Pierre-Marie Pédrot | |
| 2018-07-03 | Add overlay for equations. | Gaëtan Gilbert | |
| 2018-07-02 | Add Equations overlay | Matthieu Sozeau | |
| 2018-07-02 | Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵ | Emilio Jesus Gallego Arias | |
| points of Camlp5 | |||
| 2018-06-29 | Adding an overlay for the PR. | Pierre-Marie Pédrot | |
| 2018-06-29 | Document that GITURL variables shouldn't have a trailing .git anymore. | Théo Zimmermann | |
| This allows to append /archive at the end. | |||
| 2018-06-27 | Adding overlay. | Hugo Herbelin | |
| 2018-06-27 | Merge PR #7863: Remove Sorts.contents | Pierre-Marie Pédrot | |
| 2018-06-26 | Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵ | Pierre-Marie Pédrot | |
| constants | |||
| 2018-06-26 | Add overlay for elpi | Gaëtan Gilbert | |
| 2018-06-26 | Add overlay for Equations, Elpi | Gaëtan Gilbert | |
| 2018-06-25 | Reuse CI info to know which version of plugins to build on Windows. | Théo Zimmermann | |
| 2018-06-18 | Overlay for reference removal | Maxime Dénès | |
| 2018-06-14 | Merge PR #664: Fixing #5500 (missing test in return clause of match leading ↵ | Matthieu Sozeau | |
| to anomaly) | |||
| 2018-06-13 | Markdown docs: switch from absolute to relative links. | Théo Zimmermann | |
| We had mostly used absolute links in the past. I just discovered that GitHub recommends using relative links instead: https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links and indeed my Emacs Markdown mode can handle relative links but doesn't interpret absolute links relatively to the root of the git repository. [ci skip] | |||
| 2018-06-12 | [api] Add compatiblity Misctypes module. | Emilio Jesus Gallego Arias | |
| To be removed in 8.10. | |||
| 2018-06-05 | Merge PR #7099: Stronger invariants in unification signature. | Matthieu Sozeau | |
| 2018-06-05 | Merge PR #7495: Fix restrict_universe_context | Matthieu Sozeau | |
| 2018-06-04 | Adding an overlay for the Equations plugin. | Pierre-Marie Pédrot | |
| 2018-05-30 | overlay triggering bug #7472 (that #7495) is supposed to fix | Enrico Tassi | |
| 2018-05-27 | [api] Make `vernac/` self-contained. | Emilio Jesus Gallego Arias | |
| We make the vernacular implementation self-contained in the `vernac/` directory. To this extent we relocate the parser, printer, and AST to the `vernac/` directory, and move a couple of hint-related types to `Hints`, where they do indeed belong. IMO this makes the code easier to understand, and provides a better modularity of the codebase as now all things under `tactics` have 0 knowledge about vernaculars. The vernacular extension machinery has also been moved to `vernac/`, this will help when #6171 [proof state cleanup] is completed along with a stronger typing for vernacular interpretation that can distinguish different types of effects vernacular commands can perform. This PR introduces some very minor source-level incompatibilities due to a different module layering [thus deprecating is not possible]. Impact should be relatively minor. | |||
| 2018-05-26 | Merge PR #7543: [ide] Move common protocol library to its own folder/object. | Pierre-Marie Pédrot | |
| 2018-05-24 | [tactics] Remove anonymous fix/cofix form. | Emilio Jesus Gallego Arias | |
| We remove the `fix N / cofix N` forms from the tactic language. This way, these tactics don't depend anymore on the proof context, in particular on the proof name, which seems like a fragile practice. Apart from the concerns wrt maintenability of proof scripts, this also helps making the "proof state" functional; as we don't have to propagate the proof name to the tactic layer. | |||
| 2018-05-24 | Complete rewrite of the documentation of overlays after Jim's additional ↵ | Théo Zimmermann | |
| comments. [ci skip] | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |