| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-04-20 | overlay for elpi | Enrico Tassi | |
| 2019-04-16 | [ci] Overlays for coq/coq#9165 | Emilio Jesus Gallego Arias | |
| 2019-04-10 | Overlays for Global removal in pretyper | Maxime Dénès | |
| 2019-04-05 | Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01) | Emilio Jesus Gallego Arias | |
| Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: herbelin Ack-by: ppedrot Ack-by: proux01 | |||
| 2019-04-02 | Merge PR #8984: Declare initial hint databases in prelude | Pierre-Marie Pédrot | |
| Ack-by: JasonGross Reviewed-by: ppedrot | |||
| 2019-04-02 | Add overlays | Pierre Roux | |
| 2019-04-01 | Merge PR #9870: Minor refactoring in canonical structures | Enrico Tassi | |
| Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: ppedrot | |||
| 2019-03-31 | Add overlay | Pierre Roux | |
| 2019-03-31 | Merge PR #9733: [lexer] keyword protected quotation token for arbitrary text | Pierre-Marie Pédrot | |
| Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot | |||
| 2019-03-31 | overlay for ltac2 | Enrico Tassi | |
| 2019-03-30 | Error when [foo.(bar)] is used with nonprojection [bar] | Gaëtan Gilbert | |
| (warn if bar is a nonprimitive projection) | |||
| 2019-03-30 | Overlay for Elpi | Vincent Laporte | |
| 2019-03-27 | [proof_global] [ci] Overlays for removal of imperative state. | Emilio Jesus Gallego Arias | |
| 2019-03-26 | Overlays for HoTT, Ltac2, and UniMath | Vincent Laporte | |
| 2019-03-22 | Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ↵ | Maxime Dénès | |
| proj Ack-by: gares Reviewed-by: mattam82 Reviewed-by: maximedenes | |||
| 2019-03-20 | Add overlays for printer API changes | Maxime Dénès | |
| 2019-03-14 | Overlays for SProp | Gaëtan Gilbert | |
| 2019-03-12 | Merge PR #9389: Implement a method for manual declaration of implicits. | Emilio Jesus Gallego Arias | |
| Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: jashug | |||
| 2019-03-12 | Merge PR #7819: Ho matching occ sel | Enrico Tassi | |
| Ack-by: gares Ack-by: herbelin Ack-by: mattam82 Ack-by: ppedrot | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |