| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-06-24 | [ci] Overlays for #10316 | Emilio Jesus Gallego Arias | |
| 2019-06-24 | [proof] API Documentation fixes. | Emilio Jesus Gallego Arias | |
| 2019-06-24 | [api] [proof] Move `discharge` type to vernac_ast where it is used. | Emilio Jesus Gallego Arias | |
| This seems like the right location, a bit more refactoring should be possible. | |||
| 2019-06-24 | [api] Remove `polymorphic` type alias, use labels instead. | Emilio Jesus Gallego Arias | |
| This is more in-line with attributes and the rest of the API, and makes some code significantly clearer (as in `foo true false false`, etc...) | |||
| 2019-06-24 | [api] Move `locality` from `library` to `vernac`. | Emilio Jesus Gallego Arias | |
| This datatype does belong to this layer. | |||
| 2019-06-24 | [lemmas] [proof] Split proof kinds into per-layer components. | Emilio Jesus Gallego Arias | |
| We split `{goal,declaration,assumption}_kind` into their components. This makes sense as each part of this triple is handled by a different layer, namely: - `polymorphic` status: necessary for the lower engine layers; - `locality`: only used in `vernac` top-level constants - `kind`: merely used for cosmetic purposes [could indeed be removed / pushed upwards] We also profit from this refactoring to add some named parameters to the top-level definition API which is quite parameter-hungry. More refactoring is possible and will come in further commits, in particular this is a step towards unifying the definition / lemma save path. | |||
| 2019-06-24 | [proof] More uniformity in proof start labels. | Emilio Jesus Gallego Arias | |
| 2019-06-24 | [proof] Remove duplicated universe polymorphic from decl_kinds | Emilio Jesus Gallego Arias | |
| This information is already present on `Proof.t`, so we extract it form there. Moreover, this information is essential to the lower-level proof, as opposed to the "kind" information which is only relevant to the vernac layer; we will move it thus to its proper layer in subsequent commits. | |||
| 2019-06-24 | [proof] Remove redundant universe declaration information. | Emilio Jesus Gallego Arias | |
| This was already in the base proof object however not forwarded by `close_proof`. thus it had to be stored twice. There are more cases like this, like `poly`, all are covered by subsequent commits. | |||
| 2019-06-24 | [lemmas] Untabify. | Emilio Jesus Gallego Arias | |
| 2019-06-24 | [lemmas] Turn Lemmas.info into a proper type with constructor. | Emilio Jesus Gallego Arias | |
| Lemmas.info was a bit out of hand, as well as the parameters to the `start_*` family. Most of the info is not needed and should hopefully remain constrained to special cases, most callers only set the hook, and obligations should be better served by a `start_obligation` function soon. | |||
| 2019-06-24 | [fixpoint] Remove code duplication in (co) fixpoint declaration. | Emilio Jesus Gallego Arias | |
| 2019-06-24 | [lemmas] Reify proof information for recursive theorems. | Emilio Jesus Gallego Arias | |
| Information about interactive mutually recursive proofs was stored as a closure on an ad-hoc hook, then later made available to the hook closing actions. Instead, we put this information in the lemma state and incorporate these declarations into the normal save path. TODO: Should investigate what's going on with implicits, maybe submit a separate PR. | |||
| 2019-06-24 | [lemmas] Reify info for implicits, univ_decls, prepare for rec_thms. | Emilio Jesus Gallego Arias | |
| Key information about an interactive lemma proof was stored as a closure on an ad-hoc hook, then later made available to the hook closing actions. Instead, we put this information in the lemma state and incorporate these declarations into the normal save path. We prepare to put the information about rec_thms in the state too. | |||
| 2019-06-24 | Merge PR #10428: Remove the export_seff flag from Declare API. | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-06-24 | Remove the export_seff flag from Declare API. | Pierre-Marie Pédrot | |
| It was always the negation of the opacity flag. | |||
| 2019-06-24 | Merge PR #10406: Desynchronize the type of proof and kernel entries | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego Reviewed-by: gares | |||
| 2019-06-24 | Add overlays. | Pierre-Marie Pédrot | |
| 2019-06-24 | Code simplification for definition_entry type. | Pierre-Marie Pédrot | |
| 2019-06-24 | Remove the unused opaque_entry_inline_code field from opaque entries. | Pierre-Marie Pédrot | |
| 2019-06-24 | Enforce that opaque entries carry their type. | Pierre-Marie Pédrot | |
| 2019-06-24 | Dedicated type for opaque entries in the kernel. | Pierre-Marie Pédrot | |
| Even more invariants can be enforced this way. | |||
| 2019-06-24 | Enforce that transparent entries are forced beforehand. | Pierre-Marie Pédrot | |
| 2019-06-24 | Take advantage of the change of entry representation to split opacity status. | Pierre-Marie Pédrot | |
| Mere isomorphism for now, but will allow more invariants ultimately. | |||
| 2019-06-24 | Duplicate the type of constant entries in Proof_global. | Pierre-Marie Pédrot | |
| This allows to desynchronize the kernel-facing API from the proof-facing one. | |||
| 2019-06-24 | Move Declare to tactics folder. | Pierre-Marie Pédrot | |
| Nobody really knows where this module should belong, it seems. My personal theory is that it should live in vernac instead, but due to nasty interactions with abstract-like tactics, we have to put it somewhere below. | |||
| 2019-06-24 | Merge PR #10375: [lexer] correctly update line number when lexing QUOTATION ↵ | Pierre-Marie Pédrot | |
| (fix #10350) Ack-by: gares Reviewed-by: ppedrot | |||
| 2019-06-24 | Merge PR #10394: [ide] chop sentences taking into account QUOTATION token | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Ack-by: gares Reviewed-by: ppedrot | |||
| 2019-06-21 | Merge PR #10416: Elpi 1.4.0 | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-06-21 | Merge PR #9665: [dune] Enable optimization options in the compilation of the VM. | Théo Zimmermann | |
| Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 | |||
| 2019-06-21 | [ci] overlay for coq-elpi | Enrico Tassi | |
| 2019-06-21 | [docker] [ci] Update Elpi to version 1.4.0 | Enrico Tassi | |
| 2019-06-21 | [dune] Enable optimization options in the compilation of the VM. | Emilio Jesus Gallego Arias | |
| So far we didn't setup optimization flags for the VM in the Dune build, but time has come to experiment with such flags, we try -O3. Enabling `-flto` in the final binary build would be great, however this seems to break windows. | |||
| 2019-06-21 | Merge PR #10414: Add Conda badge to README.md | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-06-21 | Add Conda badge to README.md | Samuel Lelièvre | |
| 2019-06-20 | Merge PR #9645: [proof] Remove terminator type, unifying regular and ↵ | Pierre-Marie Pédrot | |
| obligation ones. Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot | |||
| 2019-06-19 | Merge PR #10380: [errors] remove "is_handled" logic, turn unhandled into ↵ | Gaëtan Gilbert | |
| anomalies Reviewed-by: SkySkimmer Reviewed-by: gares | |||
| 2019-06-19 | [test] unit tests for ide/coq_lex.ml | Enrico Tassi | |
| 2019-06-19 | [test-suite] support for unit-tests/ide/ tests linking coq.ide | Enrico Tassi | |
| 2019-06-19 | [META] fix dependencies of coq.ide | Enrico Tassi | |
| 2019-06-19 | [ide] chop sentences taking into account QUOTATION token | Enrico Tassi | |
| 2019-06-19 | Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations ↵ | Théo Zimmermann | |
| in favor of "simple_intropattern" Reviewed-by: Zimmi48 Reviewed-by: ppedrot | |||
| 2019-06-18 | Merge PR #10398: Revert "Fix bug #5710" | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-06-18 | [errors] remove "is_handled" logic, turn unhandled into anomalies | Emilio Jesus Gallego Arias | |
| We place the check for unhandled exceptions in the `is_anomaly` function, and consider all the exceptions non-handled by the printers always anomalies. This reworks the solution implemented in ea3909466eaaf86ff212c0a002e5df11e4a979f5 , in particular `allow_uncaught` cannot be used anymore, all exceptions must install a printer. In order to pass the test-suite CI we also had to register some printers, that were not registered for no reason, forcing clients to call a post-processing step on errors. | |||
| 2019-06-18 | Revert "Fix bug #5710" | Vincent Laporte | |
| This reverts commit 6d0083bb07528d7cd7ad2f8815d06a4e41deb16c. | |||
| 2019-06-18 | [lexer] correctly update line number when lexing QUOTATION (fix #10350) | Enrico Tassi | |
| 2019-06-18 | Merge PR #9977: [dune] Support for coqide as an ocamldebug target. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Ack-by: Zimmi48 | |||
| 2019-06-18 | Merge PR #10199: Fix computation of implicit arguments when names collide in ↵ | Maxime Dénès | |
| local fix/cofix (#10197) Reviewed-by: maximedenes | |||
| 2019-06-17 | Merge PR #10392: Fix the changelog of 8.10+beta2 following the backport of ↵ | Clément Pit-Claudel | |
| #10205. Reviewed-by: cpitclaudel | |||
| 2019-06-17 | Merge PR #10362: Kernel-side delaying of polymorphic opaque constants | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Reviewed-by: gares | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |