| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-07 | Add overlays. | Pierre-Marie Pédrot | |
| 2019-05-07 | Do not use the constant stack in whd_betaiota_deltazeta_for_iota_state. | Pierre-Marie Pédrot | |
| There is no point, it is always called with refolding turned off. | |||
| 2019-05-06 | Merge PR #10068: Coqchk: encapsulating an anomaly NotConvertible into a ↵ | Pierre-Marie Pédrot | |
| proper user-level typing error Reviewed-by: ppedrot | |||
| 2019-05-06 | Merge PR #9964: Unreleased changelog folder | Vincent Laporte | |
| Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Reviewed-by: vbgl | |||
| 2019-05-06 | Coqchk: encapsulating an anomaly NotConvertible into a proper typing error. | Hugo Herbelin | |
| Detected incidentally in "validate" check for #8893. | |||
| 2019-05-05 | Add changelog entry about moving changelog to refman. | Théo Zimmermann | |
| 2019-05-05 | [make] build unreleased.rst | Enrico Tassi | |
| 2019-05-05 | Create categories in changelog. | Théo Zimmermann | |
| 2019-05-05 | New infrastructure for the unreleased changelog. | Théo Zimmermann | |
| Move existing entries. | |||
| 2019-05-05 | Merge PR #10059: Fixing bugs introduced in change_no_check | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-05-04 | Merge PR #9926: [vernac] [ast] Make location info an attribute of vernaculars. | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot | |||
| 2019-05-04 | Merge PR #9996: Fix #5752: `Hint Mode` ignored for type classes that appear ↵ | Pierre-Marie Pédrot | |
| as assumptions Ack-by: RalfJung Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: maximedenes Reviewed-by: ppedrot Ack-by: robbertkrebbers | |||
| 2019-05-04 | Merge PR #10012: Document convert_concl_no_check (#3225) | Théo Zimmermann | |
| Reviewed-by: JasonGross Reviewed-by: Zimmi48 | |||
| 2019-05-04 | Merge PR #10057: Fix #10054: Numeral Notations without the ltac plugin. | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-05-03 | Tactics: fixing "change_no_check in". | Hugo Herbelin | |
| (Merge of the initial version with #9983 was broken) | |||
| 2019-05-03 | Updating CHANGES. | Hugo Herbelin | |
| 2019-05-03 | Merge PR #9984: Add PairUsualDecidableTypeFull | Théo Zimmermann | |
| Reviewed-by: herbelin | |||
| 2019-05-03 | Merge PR #10025: Fix #9994: `revert dependent` is extremely slow. | Vincent Laporte | |
| Ack-by: ppedrot Reviewed-by: vbgl | |||
| 2019-05-03 | Fix #9994: `revert dependent` is extremely slow. | Pierre-Marie Pédrot | |
| We add a fast path when generalizing over variables. | |||
| 2019-05-03 | Fix #10054: Numeral Notations without the ltac plugin. | Pierre-Marie Pédrot | |
| It was fairly easy, the plugin defined an argument that was only used in a vernacular extension. Thus marking it as VERNAC was enough not to link to Ltac. | |||
| 2019-05-03 | Copy-editing from code review | Jason Gross | |
| Co-Authored-By: Blaisorblade <p.giarrusso@gmail.com> | |||
| 2019-05-03 | Document _no_check tactics (#3225) | Paolo G. Giarrusso | |
| Triggered by trying to understand https://gitlab.mpi-sws.org/iris/iris/merge_requests/235. - Add a new section at the end - Document change_no_check, and convert_concl_no_check, address review comments | |||
| 2019-05-02 | Merge PR #10017: Exposing a change_no_check tactic | Pierre-Marie Pédrot | |
| Ack-by: Zimmi48 Ack-by: herbelin Reviewed-by: ppedrot | |||
| 2019-05-02 | Merge PR #10038: [comDefinition] Use prepare function from DeclareDef. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2019-05-02 | Merge PR #10047: [opam] [dune] Fix opam build by correctly setting prefix. | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-05-02 | Remove outdated comment | Maxime Dénès | |
| 2019-05-02 | Test case for #5752 | Maxime Dénès | |
| 2019-05-02 | Fix #5752: `Hint Mode` ignored for type classes that appear as assumptions | Maxime Dénès | |
| The creation of the local hint db now inherits the union of the modes from the dbs passed to `typeclasses eauto`. We could probably go further and define in a more systematic way the metadata that should be inherited. A lot of this code could also be cleaned-up by defining the merge of databases, so that the search code is parametrized by just one db (the merge of the input ones). | |||
| 2019-05-02 | Use GlobRef.Map.t in hint databases | Maxime Dénès | |
| 2019-05-02 | Add union in Map interface | Maxime Dénès | |
| 2019-05-02 | Document typeclasses_eauto | Maxime Dénès | |
| 2019-05-02 | Merge PR #10048: [CI/Azure/macOS] Fix install of OCaml through OPAM | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-05-02 | [CI/Azure/macOS] Fix install of OCaml through OPAM | Vincent Laporte | |
| 2019-05-02 | [opam] [dune] Fix opam build by correctly setting prefix. | Emilio Jesus Gallego Arias | |
| The OPAM build has been broken it seems since almost the beginning as OPAM doesn't substitute variables in the almost undocumented `build-env` form. Packages built this way worked as Coq used a different method to locate `coqlib`, however the value for `coqlib` was incorrect. We set instead the right prefix using an explicit configure call. | |||
| 2019-05-01 | Add PairUsualDecidableTypeFull | Oliver Nash | |
| A module allowing the user to build a UsualDecidableTypeFull from a pair of such, exactly analogous to the extant PairDecidableType and PairUsualDecidableType modules. Co-authored-by: Jean-Christophe Léchenet <eponier@via.ecp.fr> | |||
| 2019-05-01 | [comDefinition] Use prepare function from DeclareDef. | Emilio Jesus Gallego Arias | |
| We also update the plugin tutorial. This was already tried [in the same exact way] in #8811, however the bench time was not convincing then, but now things seem a bit better, likely due to the removal of some extra normalization somewhere. Some more changes from #8811 are still pending. | |||
| 2019-05-01 | Merge PR #10033: Remove the k0 argument from pretype functions. | Emilio Jesus Gallego Arias | |
| Reviewed-by: herbelin | |||
| 2019-04-30 | Merge PR #9947: Remove Global.env from goptions by passing from vernacentries | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-04-30 | Merge PR #10032: Remove leftover test suite file Quote.out | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-04-30 | Remove Global.env from goptions by passing from vernacentries | Gaëtan Gilbert | |
| Currently this env is only used to error for Printing If/Let on non-2-constructor/non-1-constructor types so we could alternatively remove it and not error / error later when trying to print. Keeping the env and the error as-is should be fine though. | |||
| 2019-04-30 | Remove the k0 argument from pretype functions. | Jasper Hugunin | |
| This was introduced by @herbelin in 817308ab59daa40bef09838cfc3d810863de0e46, appears to have been made unnecessary again by herbelin in 4dab4fc5b2c20e9b7db88aec25a920b56ac83cb6. At this point it appears to be completely unused. | |||
| 2019-04-30 | Remove leftover test suite file Quote.out | Gaëtan Gilbert | |
| 2019-04-30 | Merge PR #9939: Credits for 8.10 | Vincent Laporte | |
| Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: gares Ack-by: mattam82 Reviewed-by: vbgl | |||
| 2019-04-30 | Change entry from #9651. | Théo Zimmermann | |
| 2019-04-30 | Change entry for #10014. | Théo Zimmermann | |
| 2019-04-30 | Add number of commits, PRs and issues closed. | Théo Zimmermann | |
| 2019-04-30 | Advertize continuous deployment of documentation. | Théo Zimmermann | |
| 2019-04-30 | More review suggestions. | Théo Zimmermann | |
| 2019-04-30 | Remove remaining references to CHANGES.md from the Recent changes chapter. | Théo Zimmermann | |
| 2019-04-30 | Remove misplaced CHANGES entry and fix links formatting. | Théo Zimmermann | |
| PR #8187 misplaced its CHANGES entry. We remove it in this commit instead of moving it to the right place because it is reverted in #9987. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |