| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-06-25 | Re-add the "Show Goal" command for Prooftree in PG. | Jim Fehrle | |
| It prints a goal given its internal goal id and the Stm state id. | |||
| 2019-06-25 | Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec ↵ | Pierre-Marie Pédrot | |
| theorems. Reviewed-by: SkySkimmer Ack-by: ejgallego Reviewed-by: gares Reviewed-by: ppedrot | |||
| 2019-06-25 | Merge PR #10219: [Ltac2] Add util files for Bool, List, Option | Pierre-Marie Pédrot | |
| Ack-by: JasonGross Ack-by: MSoegtropIMC Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ppedrot | |||
| 2019-06-25 | Merge PR #10162: Fix #10161: occur check when defining an algebraic universe. | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Ack-by: mattam82 Reviewed-by: ppedrot | |||
| 2019-06-25 | Merge PR #10284: Expose set interface to option tables | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Reviewed-by: ejgallego Reviewed-by: ppedrot | |||
| 2019-06-25 | Merge PR #10412: Add output-coqtop test directory that runs output tests ↵ | Enrico Tassi | |
| with coqtop Reviewed-by: gares Ack-by: jfehrle | |||
| 2019-06-25 | Merge PR #10408: Fix coqdoc title: should be on a single line. | Vincent Laporte | |
| Reviewed-by: vbgl | |||
| 2019-06-24 | [proof] Remove last case of optional `?poly` arguments. | Emilio Jesus Gallego Arias | |
| As noted in GitHub discussion, it is a good idea to make `poly` always explicit, this PR does remove last case of `?(poly=false)` in the codebase. | |||
| 2019-06-24 | Use named records instead of tuples where `polymorphic` used to be. | Gaëtan Gilbert | |
| Followup on "[api] Remove `polymorphic` type alias, use labels instead." | |||
| 2019-06-24 | [proof] dev/doc/changes for the last refactorings | Emilio Jesus Gallego Arias | |
| 2019-06-24 | [proof] Move initial_euctx to proof_global | Emilio Jesus Gallego Arias | |
| These are only needed when closing / admitting a proof. | |||
| 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 | Add output-coqtop test directory that runs output tests with coqtop | Jim Fehrle | |
| 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-20 | Fix coqdoc title: should be on a single line. | Théo Zimmermann | |
| Otherwise coqdoc doesn't understand it is still the title. | |||
| 2019-06-19 | Merge PR #10380: [errors] remove "is_handled" logic, turn unhandled into ↵ | Gaëtan Gilbert | |
| anomalies Reviewed-by: SkySkimmer Reviewed-by: gares | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |