| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-14 | Merge PR #8893: Moving evars_of_term from constr to econstr | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Reviewed-by: gares Ack-by: herbelin Reviewed-by: maximedenes Reviewed-by: ppedrot | |||
| 2019-05-14 | Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2 | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Reviewed-by: ppedrot | |||
| 2019-05-14 | Merge PR #10135: Make detyping robust w.r.t. indexed anonymous variables | Pierre-Marie Pédrot | |
| Ack-by: ejgallego Ack-by: maximedenes Reviewed-by: ppedrot | |||
| 2019-05-14 | Overlay for value-returning run_tactic | Gaëtan Gilbert | |
| 2019-05-13 | Adding overlay for Equations. | Hugo Herbelin | |
| 2019-05-13 | Merge PR #10076: [Canonical structures] Annotation to field declarations to ↵ | Enrico Tassi | |
| prevent them from being “canonical” Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes Ack-by: robbertkrebbers Ack-by: vbgl | |||
| 2019-05-13 | Add overlay for Unicoq | Maxime Dénès | |
| 2019-05-10 | Add overlay for elpi | Vincent Laporte | |
| 2019-05-10 | Add overlays for coq/coq#10052. | Pierre-Marie Pédrot | |
| 2019-05-07 | Add overlays. | Pierre-Marie Pédrot | |
| 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` | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |