| Age | Commit message (Expand) | Author |
|---|
| 2020-09-23 | Merge PR #12977: Statically ensure that only polymophic hint terms come with ... | coqbot-app[bot] |
| 2020-09-23 | Merge PR #13073: A temporary fix of #13018 and #12775 for branch 8.12 (bis) | coqbot-app[bot] |
| 2020-09-15 | [vernac] Don't allow attributes on print / check | Emilio Jesus Gallego Arias |
| 2020-09-15 | A temporary fix of #13018 and #12775 for branch 8.2. | Hugo Herbelin |
| 2020-09-13 | Statically ensure that only polymophic hint terms come with a context. | Pierre-Marie Pédrot |
| 2020-09-10 | When a notation is only parsing, do not attach to it a specific format. | Hugo Herbelin |
| 2020-09-09 | Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable fro... | Pierre-Marie Pédrot |
| 2020-09-08 | Merge PR #12931: Proof using cleanup, small doc addition and fix using Type i... | coqbot-app[bot] |
| 2020-09-07 | Circumvent revealed bug of evar resolution for fixpoint | Maxime Dénès |
| 2020-09-03 | Fix incorrect debruijn handling when Record calls maybe_unify_params_in | Gaëtan Gilbert |
| 2020-09-01 | Unify the shelves | Maxime Dénès |
| 2020-09-01 | Merge PR #12892: Update update_global_env usage | Pierre-Marie Pédrot |
| 2020-08-31 | [declare] Return both declared constants in Derive path. | Emilio Jesus Gallego Arias |
| 2020-08-31 | Update update_global_env usage | Gaëtan Gilbert |
| 2020-08-28 | About: Add a mention that arguments have been renamed, if ever it is the case. | Hugo Herbelin |
| 2020-08-28 | Where there are several lists of implicit arguments, don't pretend names matter. | Hugo Herbelin |
| 2020-08-28 | Do not write "rename" for arguments in About, since these arguments are valid... | Hugo Herbelin |
| 2020-08-28 | When printing the type in About, use the renamed arguments. | Hugo Herbelin |
| 2020-08-28 | When reporting an implicit argument error on a rename argument, use the renam... | Hugo Herbelin |
| 2020-08-28 | In "About", print all arguments, even if it is trailing list of _. | Hugo Herbelin |
| 2020-08-28 | Proof using cleanup, small doc addition and fix using Type in collections | Gaëtan Gilbert |
| 2020-08-27 | [state] A few nits after consolidation of state. | Emilio Jesus Gallego Arias |
| 2020-08-27 | Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfoo | Pierre-Marie Pédrot |
| 2020-08-26 | Wrap future goals into a module | Maxime Dénès |
| 2020-08-26 | Make future_goals stack explicit in the evarmap | Maxime Dénès |
| 2020-08-26 | Move given_up goals to evar_map | Maxime Dénès |
| 2020-08-25 | Moving production_level_eq to extend.ml for separation of concerns. | Hugo Herbelin |
| 2020-08-25 | A fix and two enhancements of trailing pattern factorization in rec. notations. | Hugo Herbelin |
| 2020-08-25 | Fix slow Print Universes Subgraph when many ambient universes. | Gaëtan Gilbert |
| 2020-08-24 | Update sigma instead of erasing it in `update_global_env` | Maxime Dénès |
| 2020-08-22 | Merge PR #12866: Less fragile scheme equality | Hugo Herbelin |
| 2020-08-21 | Merge PR #12759: [vernac] refine check for unresolved evars | coqbot |
| 2020-08-20 | Use properly fresh names for Scheme Equality | Jasper Hugunin |
| 2020-08-20 | Merge PR #12756: Do not refresh the names of implicit arguments. | Maxime Dénès |
| 2020-08-20 | [vernac] refine check for unresolved evars | Enrico Tassi |
| 2020-08-19 | Do not refresh the names of implicit arguments. | Jasper Hugunin |
| 2020-08-18 | Rename VM-related kernel/cfoo files to kernel/vmfoo | Gaëtan Gilbert |
| 2020-07-26 | Merge PR #12726: Clarify Global.env usage in ppvernac | Pierre-Marie Pédrot |
| 2020-07-26 | Merge PR #12573: Hint Opaque/Transparent/Unfold: don't error on Opaque Define... | Pierre-Marie Pédrot |
| 2020-07-23 | Merge PR #12678: Tweak the warning for arbitrary term hints. | Emilio Jesus Gallego Arias |
| 2020-07-23 | Hint Opaque/Transparent/Unfold: don't error on opaque constants | Gaëtan Gilbert |
| 2020-07-22 | Clarify Global.env usage in ppvernac | Gaëtan Gilbert |
| 2020-07-22 | Merge PR #12664: Turn various anomalies into regular errors in primitive decl... | Pierre-Marie Pédrot |
| 2020-07-21 | Merge PR #12714: [declare] Remove some dead code in declare_mutual_definition | Gaëtan Gilbert |
| 2020-07-21 | Turn various anomalies into regular errors in primitive declaration path | Gaëtan Gilbert |
| 2020-07-21 | Merge PR #12697: Fix bug #12691: an only-parsing notation needs to produce a ... | Emilio Jesus Gallego Arias |
| 2020-07-20 | [declare] Remove some dead code in declare_mutual_definition | Emilio Jesus Gallego Arias |
| 2020-07-18 | Merge PR #12588: [exn] Remove some uses of print | Pierre-Marie Pédrot |
| 2020-07-17 | Remove automatic formatting of ComHints. | Pierre-Marie Pédrot |
| 2020-07-17 | Tweak the warning for arbitrary term hints. | Pierre-Marie Pédrot |
