aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc
Commit message (Collapse)AuthorAge
* [ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Gravatar Emilio Jesus Gallego Arias2018-07-11
| | | | | | - We update the OCaml version used in the base CI image. - Windows / OSX image building is also updated to use newer OCaml. - We also update Dune to 1.0.0.
* Merge PR #7898: Remove camlp4 remainsGravatar Emilio Jesus Gallego Arias2018-07-11
|\
* | Modify URLs in xml-protocol.mdGravatar Rin Arakaki2018-07-08
| |
* | Modify URLs in xml-protocol.mdGravatar Rin Arakaki2018-07-08
| |
| * Introduce a Pcoq.Entry module for functions that ought to be exported.Gravatar Pierre-Marie Pédrot2018-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.
* Merge PR #7979: TACTIC EXTEND in coqppGravatar Emilio Jesus Gallego Arias2018-07-05
|\
| * Documenting the syntax changes.Gravatar Pierre-Marie Pédrot2018-07-02
| |
* | Clean up documentation around beginner's guide.Gravatar Siddharth Bhat2018-07-02
|/ | | | | | | | | - move `README` to `README.md` to take advantage of markdown features - remove `setup.txt`, port the editor specific information to the wiki. Merge development information into `dev/doc/README.md`. Wiki merge link: https://github.com/coq/coq/wiki/DevelSetup. - Add new links to files into `dev/README.md`. - Remove stale `translate.txt`.
* Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵Gravatar Emilio Jesus Gallego Arias2018-07-02
|\ | | | | | | points of Camlp5
* \ Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, ↵Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ \ | | | | | | | | | Z into three files
| | * Documenting the transition strategy of GEXTEND.Gravatar Pierre-Marie Pédrot2018-06-29
| |/ |/|
* | Merge PR #7918: Mini-update of version history with recent changes.Gravatar Théo Zimmermann2018-06-29
|\ \
| | * Splitting primitive numeral parser/printer for positive, N, Z into three files.Gravatar Hugo Herbelin2018-06-29
| | |
* | | Merge PR #7080: Swapping Context and Constr and defining declarations on ↵Gravatar Maxime Dénès2018-06-29
|\ \ \ | |_|/ |/| | | | | constr in Constr
| * | Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | This shall eventually allow to use contexts of declarations in the definition of the "Case" constructor. Basically, this means that Constr now includes Context and that the "t" types of Context which were specialized on constr are not defined in Constr (unfortunately using a heavy boilerplate).
| | * Mini-update of version history with recent changes.Gravatar Hugo Herbelin2018-06-25
| |/
* / Critical bugs: added #3243 and Gonthier's bug in lazy machine.Gravatar Hugo Herbelin2018-06-25
|/ | | | Both reminded by Enrico.
* Merge PR #7805: Towards listing the critical bugs of the history of Coq.Gravatar Théo Zimmermann2018-06-24
|\
* \ Merge PR #7774: [build] Fix checks and notes noting 4.02.1 instead of 4.02.3Gravatar Maxime Dénès2018-06-21
|\ \
* | | Remove reference name type.Gravatar Maxime Dénès2018-06-18
| | | | | | | | | | | | | | | | | | | | | | | | reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
| | * Very first try at listing the critical bugs of the history of Coq.Gravatar Hugo Herbelin2018-06-15
| |/ |/| | | | | | | | | | | | | | | I let open several questions about fixes to the kernel which maybe were not critical. I skipped what seemed to have been bugs in beta-releases. Need double-checks, decision about the format, etc.
* | Document how to restart failed CI jobs.Gravatar Théo Zimmermann2018-06-13
| | | | | | | | [ci skip]
* | Markdown docs: switch from absolute to relative links.Gravatar Théo Zimmermann2018-06-13
| | | | | | | | | | | | | | | | | | | | 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]
| * [build] Fix checks and notes noting 4.02.1 instead of 4.02.3Gravatar Emilio Jesus Gallego Arias2018-06-11
|/ | | | | Bumping to 4.02.3 was decided some time ago in the WG, however a couple of places escaped updating.
* dev/doc/univpoly.{txt => md}, split off primitive projection infoGravatar Gaëtan Gilbert2018-06-08
|
* Documenting the API change.Gravatar Pierre-Marie Pédrot2018-06-04
|
* [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-05-31
| | | | | | | | | | | | | | | | | | Continuing the interface cleanup we place `Constrexpr` in the internalization module, which is the one that eliminates it. This slims down `pretyping` considerably, including removing the `Univdecls` module which existed only due to bad dependency ordering in the first place. Thanks to @ Skyskimmer we also remove a duplicate `univ_decl` definition among `Misctypes` and `UState`. This is mostly a proof of concept yet as it depends on quite a few patches of the tree. For sure some tweaks will be necessary, but it should be good for review now. IMO the tree is now in a state where we can could easy eliminate more than 10 modules without any impact, IMHO this is a net saving API-wise and would help people to understand the structure of the code better.
* [api] Make `vernac/` self-contained.Gravatar Emilio Jesus Gallego Arias2018-05-27
| | | | | | | | | | | | | | | | | | | | 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.
* Merge PR #7573: Remove unused Printer.printer_pr override mechanism.Gravatar Hugo Herbelin2018-05-27
|\
* \ Merge PR #6057: Start a release process documentation.Gravatar Maxime Dénès2018-05-26
|\ \
* \ \ Merge PR #7574: Improve merging and overlay documentations.Gravatar Emilio Jesus Gallego Arias2018-05-24
|\ \ \
| | | * Remove the unused printer_pr mechanism.Gravatar Jim Fehrle2018-05-24
| |_|/ |/| |
| * | Complete rewrite of the documentation of overlays after Jim's additional ↵Gravatar Théo Zimmermann2018-05-24
| | | | | | | | | | | | | | | | | | comments. [ci skip]
| * | Improve merging and overlay documentations.Gravatar Théo Zimmermann2018-05-24
| | | | | | | | | | | | | | | | | | Clarification prompted by Jim Fehrle. [ci skip]
* | | Document Smart/Array changes in dev/doc/Changes.md.Gravatar Hugo Herbelin2018-05-23
|/ /
* | Merge PR #6965: [api] Move universe syntax to `Glob_term`Gravatar Pierre-Marie Pédrot2018-05-18
|\ \
| | * Create a documentation for the release manager.Gravatar Théo Zimmermann2018-05-18
| |/ |/| | | | | | | | | This process is expected to evolve in the future as we automate it more and more. [ci skip]
* | add unit tests to test suiteGravatar Paul Steckler2018-05-16
| |
* | Update MERGING.mdGravatar Matthieu Sozeau2018-05-15
| | | | | | Simpler
* | Update MERGING.mdGravatar Matthieu Sozeau2018-05-15
| | | | | | Actually there are more general instructions
* | git / gpg integration linkGravatar Matthieu Sozeau2018-05-15
| |
| * [api] Move universe syntax to `Glob_term`Gravatar Emilio Jesus Gallego Arias2018-05-08
|/ | | | | | | | | | | | | We move syntax for universes from `Misctypes` to `Glob_term`. There is basically no reason that this type is there instead of the proper file, as witnessed by the diff. Unfortunately the change is not compatible due to moving a type to a higher level in the hierarchy, but we expect few problems. This change plus the related PR (#6515) moving universe declaration to their proper place make `Misctypes` into basically an empty file save for introduction patterns.
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
| | | | | | | | | | | | | In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at.
* Merge PR #7290: Update debugging.mdGravatar Hugo Herbelin2018-04-25
|\
* | [api] Relocate `intf` modules according to dependency-order.Gravatar Emilio Jesus Gallego Arias2018-04-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In a component-based source code organization of Coq `intf` doesn't fit very well, as it sits in bit of "limbo" between different components, and indeed, encourages developers to place types in sometimes random places wrt the hierarchy. For example, lower parts of the system reference `Vernacexpr`, which morally lives in a pretty higher part of the system. We move all the files in `intf` to the lowest place their dependencies can accommodate: - `Misctypes`: is used by Declaremod, thus it has to go in `library` or below. Ideally, this file would disappear. - `Evar_kinds`: it is used by files in `engine`, so that seems its proper placement. - `Decl_kinds`: used in `library`, seems like the right place. [could also be merged. - `Glob_term`: belongs to pretyping, where it is placed. - `Locus`: ditto. - `Pattern`: ditto. - `Genredexpr`: depended by a few modules in `pretyping`, seems like the righ place. - `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and could be fixed, as this module should be declared in `interp` which is the one eliminating it. - `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed as it contains stuff it shouldn't. The right place should be `parsing`. - `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`. - `Notation_term`: First place used is `interp`, seems like the right place. Additionally, for some files it could be worth to merge files of the form `Foo` with `Foo_ops` in the medium term, as to create proper ADT modules as done in the kernel with `Name`, etc...
* | Merge PR #7240: [doc] [engine] Document `abort_on_undefined_evars`.Gravatar Pierre-Marie Pédrot2018-04-23
|\ \
* \ \ Merge PR #7219: merge script support https + typos in docGravatar Maxime Dénès2018-04-19
|\ \ \
| | | * Update debugging.mdGravatar Jasper Hugunin2018-04-15
| |_|/ |/| | | | | This changed in https://github.com/coq/coq/commit/35961a4ff5a5b8c9b9786cbab0abd279263eb655
| | * [doc] [engine] Document `abort_on_undefined_evars`.Gravatar Emilio Jesus Gallego Arias2018-04-15
| |/ |/|
* | Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
| | | | | | | | | | | | We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr.