| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-06-13 | Merge PR #10319: [STM] Only VtSideeff can be VtNow/VtLater | Enrico Tassi | |
| Ack-by: ejgallego Reviewed-by: gares | |||
| 2019-06-12 | Merge PR #10358: [docker] update elpi to 1.3.1 | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2019-06-11 | overlay | Enrico Tassi | |
| 2019-06-11 | Adding an overlay for Equations. | Pierre-Marie Pédrot | |
| 2019-06-11 | Overlays for 10319 | Gaëtan Gilbert | |
| 2019-06-09 | [ci] Overlays for move_termination_routine_out | Emilio Jesus Gallego Arias | |
| 2019-06-08 | Overlays for Elpi + Equations + Mtac2 + fiat parsers + paramcoq. | Hugo Herbelin | |
| 2019-06-06 | Remove old overlays | Gaëtan Gilbert | |
| I updated the readme example using the most recent overlay with only 1 touched development. | |||
| 2019-06-06 | Merge PR #8988: Towards unifying parsing/printing for universe instances and ↵ | Gaëtan Gilbert | |
| Type's argument Reviewed-by: SkySkimmer Reviewed-by: gares Reviewed-by: mattam82 Reviewed-by: maximedenes | |||
| 2019-06-04 | update overlays | Enrico Tassi | |
| 2019-06-04 | Overlays for coq/coq#10050 (proof_global API changes) | Gaëtan Gilbert | |
| 2019-06-01 | Adding overlay for elpi | Hugo Herbelin | |
| 2019-05-27 | Overlay for mind_kelim change (#10133) | Gaëtan Gilbert | |
| 2019-05-24 | Adding overlays. | Pierre-Marie Pédrot | |
| 2019-05-23 | Merge PR #9895: [loadpath] Make loadpath handling self-contained and move to ↵ | Maxime Dénès | |
| vernac Reviewed-by: maximedenes | |||
| 2019-05-23 | Merge PR #10185: Remove undocumented Instance : ! syntax | Vincent Laporte | |
| Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: vbgl | |||
| 2019-05-22 | Merge PR #10177: Fix #10176: shadowing vs automatic class based ↵ | Hugo Herbelin | |
| generalization + cleanups Reviewed-by: herbelin | |||
| 2019-05-21 | [loadpath] Further cleanup after merge with MlTop. | Emilio Jesus Gallego Arias | |
| We cleanup a bit the implementation of LoadPath which is not possible as now all the loadpath logic is in the same place. In particular, we remove exceptions in favor a `locate_result` monad. More cleanup should still be possible, in particular `locate_absolute_library` and `locate_qualified_library` should be merged. | |||
| 2019-05-21 | Overlay for definition-not-visible overhaul | Gaëtan Gilbert | |
| 2019-05-21 | Overlay for removing Instance: !type syntax | Gaëtan Gilbert | |
| 2019-05-17 | Overlay for removing Generalized 1st arg | Gaëtan Gilbert | |
| 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 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |