| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-27 | Adding overlay for ltac2. | Hugo Herbelin | |
| 2017-11-27 | Merge PR #6227: Linter: do not lint untracked files. | Maxime Dénès | |
| 2017-11-26 | [api] Remove aliases of `Evar.t` | Emilio Jesus Gallego Arias | |
| There don't really bring anything, we also correct some minor nits with the printing function. | |||
| 2017-11-25 | Overlay for stronger restrict_universe_context. | Gaëtan Gilbert | |
| 2017-11-24 | Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion | Maxime Dénès | |
| 2017-11-24 | Merge PR #6197: [plugin] Remove LocalityFixme über hack. | Maxime Dénès | |
| 2017-11-23 | Merge PR #6186: [api] Miscellaneous consolidation. | Maxime Dénès | |
| 2017-11-23 | Linter: do not lint untracked files. | Gaëtan Gilbert | |
| 2017-11-23 | Adding ad hoc overlay for sf/vfa. | Hugo Herbelin | |
| 2017-11-23 | Merge PR #6189: Disable whitespace linter for .out files. | Maxime Dénès | |
| 2017-11-22 | [plugin] Remove LocalityFixme über hack. | Emilio Jesus Gallego Arias | |
| To that extent we introduce a new prototype vernacular extension macro `VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the proper parameters and attributes. This of course needs more refinement, in particular we should move `vernac_command` to its own file and make `Vernacentries` consistent wrt it. | |||
| 2017-11-21 | [api] Miscellaneous consolidation + moves to engine. | Emilio Jesus Gallego Arias | |
| We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization. | |||
| 2017-11-21 | [printing] Deprecate all printing functions accessing the global proof. | Emilio Jesus Gallego Arias | |
| We'd like to handle proofs functionally we thus recommend not to use printing functions without an explicit context. We also adapt most of the code, making more explicit where the printing environment is coming from. An open task is to refactor some code so we gradually make the `Pfedit.get_current_context ()` disappear. | |||
| 2017-11-21 | Merge PR #6185: [parser] Remove unnecessary statically initialized hook. | Maxime Dénès | |
| 2017-11-21 | Merge PR #6168: Add Equations to CI | Maxime Dénès | |
| 2017-11-20 | Disable whitespace linter for .out files. | Gaëtan Gilbert | |
| 2017-11-20 | Merge PR #6183: [plugins] Prepare plugin API for functional handling of state. | Maxime Dénès | |
| 2017-11-20 | Merge PR #6163: [dev] Remove deprecation warning from `base_include` | Maxime Dénès | |
| 2017-11-20 | Add Equations to CI | Matthieu Sozeau | |
| 2017-11-19 | [parser] Remove unnecessary statically initialized hook. | Emilio Jesus Gallego Arias | |
| Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to put any pattern in binders, prefixed by a quote."] its current placement as well as the hook don't make a lot of sense. In particular, they prevent parts of Coq working without linking the parser. To this purpose, we need to consolidate the `Constrexpr` utilities. While we are at it we do so and remove the `Topconstr` module which is fully redundant with `Constrexpr_ops`. | |||
| 2017-11-19 | [plugins] Prepare plugin API for functional handling of state. | Emilio Jesus Gallego Arias | |
| To this purpose we allow plugins to register functions that will modify the state. This is not used yet, but will be used soon when we remove the global handling of the proof state. | |||
| 2017-11-16 | Merge PR #6148: [api] Another large deprecation, `Nameops` and friends. | Maxime Dénès | |
| 2017-11-15 | [dev] Remove deprecation warning from `base_include` | Emilio Jesus Gallego Arias | |
| The warning created problems as OCaml restored the color printing tags when printing it, so users doing `Drop` and then `go ()` got color printing back after the warning. We should guard the console on `Drop` better, but this requires some (much needed) refactoring work in the toplevel. | |||
| 2017-11-13 | [api] Another large deprecation, `Nameops` | Emilio Jesus Gallego Arias | |
| 2017-11-13 | Change OCAMLRUNPARAM warning to mention OCaml 4.06 | Paul Steckler | |
| 2017-11-13 | Merge PR #6098: [api] Move structures deprecated in the API to the core. | Maxime Dénès | |
| 2017-11-13 | Merge PR #6126: Fix ci-bignums.sh "missing ]" error. | Maxime Dénès | |
| 2017-11-13 | Merge PR #6124: Adding a debugging printer for ident maps whose codomain ↵ | Maxime Dénès | |
| type is unknown | |||
| 2017-11-13 | Merge PR #6071: [ci] Add Ltac2 | Maxime Dénès | |
| 2017-11-13 | Merge PR #6065: [api] Deprecate all legacy uses of Names in core. | Maxime Dénès | |
| 2017-11-09 | Fix ci-bignums.sh "missing ]" error. | Gaëtan Gilbert | |
| It made the test always fail so ci-common was always sourced. It's not quite idempotent as it adds COQBIN to PATH but it didn't lead to CI failure. | |||
| 2017-11-08 | Adding a debugging printer for ident maps whose codomain type is unknown. | Hugo Herbelin | |
| Actually, ocaml is apparently doing well. If there is a printer for 'a Id.Map.t and another for say Id.t Id.Map.id, it uses the most defined existing ones, so, it is apparently not a problem to have overlapping printer. | |||
| 2017-11-08 | Merge PR #6100: [api] Remove 8.7 ML-deprecated functions. | Maxime Dénès | |
| 2017-11-08 | Merge PR #6086: [ci] Switch VST back to upstream. | Maxime Dénès | |
| 2017-11-07 | [api] Remove 8.7 ML-deprecated functions. | Emilio Jesus Gallego Arias | |
| 2017-11-06 | [api] Move structures deprecated in the API to the core. | Emilio Jesus Gallego Arias | |
| We do up to `Term` which is the main bulk of the changes. | |||
| 2017-11-06 | [api] Deprecate all legacy uses of Names in core. | Emilio Jesus Gallego Arias | |
| This will allow to merge back `Names` with `API.Names` | |||
| 2017-11-06 | Merge PR #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" ↵ | Maxime Dénès | |
| rules | |||
| 2017-11-06 | Merge PR #1139: Add a linter. | Maxime Dénès | |
| 2017-11-04 | [ci] Add Ltac2 | Jason Gross | |
| 2017-11-03 | Merge PR #6047: A generic printer for ltac values | Maxime Dénès | |
| 2017-11-03 | Merge PR #6036: [toplevel] Export the last document seen after `Drop`. | Maxime Dénès | |
| 2017-11-03 | Merge PR #6031: [ci] Switch back to upstream version of Math-Classes and Corn. | Maxime Dénès | |
| 2017-11-03 | Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in ↵ | Maxime Dénès | |
| dev/doc/changes. | |||
| 2017-11-03 | Merge PR #6024: Update of Coq version history | Maxime Dénès | |
| 2017-11-02 | Using a specific function to register vernac printers. | Hugo Herbelin | |
| 2017-11-01 | provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules | Matej Košík | |
| Originally, it was not possible to define a new vernacular command in the following way: VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY [ "SomeCmd" ] -> [ Feedback.msg_notice ?loc (Pp.str "some message") ] END because "loc : Loc.t" was not bound. This commit fixes that, i.e. the location of the custom Vernacular command (within *.v file) is made available as "loc" variable bound on the right side of "->" . | |||
| 2017-10-30 | [ci] Switch VST back to upstream. | Théo Zimmermann | |
| This finally closes #5994. | |||
| 2017-10-28 | [toplevel] Export the last document seen after `Drop`. | Emilio Jesus Gallego Arias | |
| After `Drop`, `Coqtop.drop_last_doc` will contain the current document used by `Coqloop`. This is useful for people wanting to restart Coq after a `Drop`. | |||
| 2017-10-27 | [ci] Switch back to upstream version of Math-Classes and Corn. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |