| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-02-28 | Constructor type information uses the expanded form. | Pierre-Marie Pédrot | |
| It used to simply remember the normal form of the type of the constructor. This is somewhat problematic as this is ambiguous in presence of let-bindings. Rather, we store this data in a fully expanded way, relying on rel_contexts. Probably fixes a crapload of bugs with inductive types containing let-bindings, but it seems that not many were reported in the bugtracker. | |||
| 2019-02-28 | Overlays for coq/coq#9389 implicits API cleanup | Gaëtan Gilbert | |
| 2019-02-23 | [vernac] Unify declaration hooks. | Emilio Jesus Gallego Arias | |
| Supersedes #8718. | |||
| 2019-02-22 | overlay for Equations | Enrico Tassi | |
| 2019-02-17 | Separate variance and universe fields in inductives. | Gaëtan Gilbert | |
| I think the usage looks cleaner this way. | |||
| 2019-02-12 | [tactics] Remove dependency of abstract on global proof state. | Emilio Jesus Gallego Arias | |
| In order to do so we place the polymorphic status and name in the read-only part of the monad. Note the added comments, as well as the fact that almost no part of tactics depends on `proofs` nor `interp`, thus they should be placed just after pretyping. Gaëtan Gilbert noted that ideally, abstract should not depend on the polymorphic status, should we be able to defer closing of the constant, however this will require significant effort. Also, we may deprecate nameless abstract, thus rending both of the changes this PR need unnecessary. | |||
| 2019-02-08 | Update overlay file | Matthieu Sozeau | |
| 2019-02-08 | Add overlay for Equations | Matthieu Sozeau | |
| 2019-02-08 | Add overlays for unicoq and mtac2 | Matthieu Sozeau | |
| 2019-02-05 | Overlays | Maxime Dénès | |
| 2019-02-04 | Overlays. | Maxime Dénès | |
| 2019-01-24 | Add Overlays | Maxime Dénès | |
| 2018-12-17 | Merge PR #9153: [api] Move reduction modules to `tactics` | Pierre-Marie Pédrot | |
| 2018-12-17 | Merge PR #9220: Move shallow state logic to the function preparing state for ↵ | Enrico Tassi | |
| workers | |||
| 2018-12-14 | [proof] Rework proof interface. | Emilio Jesus Gallego Arias | |
| - deprecate the old 5-tuple accessor in favor of a view record, - move `name` and `kind` proof data from `Proof_global` to `Proof`, this will prove useful in subsequent functionalizations of the interface, in particular this is what abstract, which lives in the monads, needs in order no to access global state. - Note that `Proof.t` and `Proof_global.t` are redundant anyways. | |||
| 2018-12-13 | Add overlay | Maxime Dénès | |
| 2018-12-11 | [ci] Clean overlay folder. | Emilio Jesus Gallego Arias | |
| 2018-12-09 | [doc] Enable Warning 50 [incorrect doc comment] and fix comments. | Emilio Jesus Gallego Arias | |
| This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :) | |||
| 2018-12-05 | Merge PR #9065: [gramlib] Remove `Ploc.t` in favor of `Loc.t` | Pierre-Marie Pédrot | |
| 2018-11-30 | [vernac] [hooks] Refactor towards optional hooks. | Emilio Jesus Gallego Arias | |
| We make `declaration_hook`s optional arguments everywhere, and thus we avoid some "fake" functions having to be passed. This identifies positively the code really using hooks [funind, rewrite, coercions, program, and canonicals] and helps moving toward some hope of reification. | |||
| 2018-11-30 | [gramlib] Remove `Ploc.t` in favor of `Loc.t` | Emilio Jesus Gallego Arias | |
| The types are identical and we have no more reason for the split. Note the following TODOS: - discrepancy of `Ploc.after` with `CLexer.after` - discrepancy of `Ploc.comments` with `CLexer.comments` - `Ploc.dummy` vs `Loc.t option` | |||
| 2018-11-28 | [ltac] Remove aliases already present in the lower layers. | Emilio Jesus Gallego Arias | |
| We remove a few aliases present in the lower layers [`Genintern/Tactypes`] from `Tacexpr`. IMHO this enlarges the API for no good purpose, and difficults analysis. | |||
| 2018-11-27 | Merge PR #8850: Private universes for opaque polymorphic constants. | Matthieu Sozeau | |
| 2018-11-24 | Merge PR #8933: Make initial evar map argument to check_evars_are_solved ↵ | Pierre-Marie Pédrot | |
| optional. | |||
| 2018-11-23 | Adding overlay. | Pierre-Marie Pédrot | |
| 2018-11-23 | Overlay for private polymorphic universes | Gaëtan Gilbert | |
| 2018-11-21 | Merge PR #8985: [gramlib] [build] Switch make-based system to packed gramlib | Enrico Tassi | |
| 2018-11-21 | Add overlay for solve-remaining-evars-initial-arg | Gaëtan Gilbert | |
| 2018-11-21 | [legacy proof engine] Remove some cruft. | Emilio Jesus Gallego Arias | |
| We remove the `Proof_types` file which was a trivial stub, we also cleanup a few layers of aliases. This is not a lot but every little step helps. | |||
| 2018-11-21 | [gramlib] [build] Switch make-based system to packed gramlib | Emilio Jesus Gallego Arias | |
| This makes the make-based build system stop linking to Camlp5's gramlib and instead links to our own gramlib. We use the style done in the packing of `Stdlib` in OCaml 4.07. As to introduce a minimal amount of noise in history we use an autogenerated `gramlib__pack` directory. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2018-11-20 | Merge PR #7925: Clean transparent state | Maxime Dénès | |
| 2018-11-19 | Merge PR #9003: [vernacextend] Consolidate extension points API | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #8902: [ltac] Use CAst nodes in the tactic AST. | Pierre-Marie Pédrot | |
| 2018-11-19 | Adding overlays. | Pierre-Marie Pédrot | |
| 2018-11-18 | Merge PR #9018: [devtools] Small script to setup overlays automatically | Gaëtan Gilbert | |
| 2018-11-17 | [vernacextend] Consolidate extension points API | Emilio Jesus Gallego Arias | |
| We group the extension API and datatypes under `Vernacextend`. This means that the base plugin dependency is now `coq.vernac` from `coq.stm`. This is quite important as for example the LSP server won't like to link the STM in. LTAC still depends on the STM by means of the ltac_profile part tho. The next step could be to move the extension point below `Vernacexpr`. | |||
| 2018-11-17 | [ci] Cleanup of old overlays. | Emilio Jesus Gallego Arias | |
| 2018-11-17 | [CoqProject] Abstract warning function for CoqProject readers. | Emilio Jesus Gallego Arias | |
| `CoqProject_file` uses the feedback system, however this is not very convenient in some scenarios such as `coqdep` that has to be run very early in the build process [and thus in "boot" mode]. We thus make the warning function a paramater. Should fix #8913. | |||
| 2018-11-17 | [ltac] Use CAst nodes in the tactic AST. | Emilio Jesus Gallego Arias | |
| This provides several advantages to people serializing tactic scripts. Appearance of the involved constructors is common enough as to bother to submit this PR. | |||
| 2018-11-16 | Remove the implicit tactic feature following #7229. | Pierre-Marie Pédrot | |
| 2018-11-09 | Adding an overlay for #8601. | Pierre-Marie Pédrot | |
| 2018-11-06 | Add overlay for Equations | Matthieu Sozeau | |
| 2018-11-05 | Merge PR #8515: Command driven attributes | Pierre-Marie Pédrot | |
| 2018-11-03 | Merge PR #8844: Move abstract out of tactics.ml | Pierre-Marie Pédrot | |
| 2018-11-02 | Add overlays (command driven attributes) | Gaëtan Gilbert | |
| 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 | Overlays (#8844 split-tactics) | 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |