aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2020-10-08Merge PR #12949: When a notation is only parsing, do not attach to it a speci...coqbot-app[bot]
2020-10-06Define a new type instance_flag instead of using [unit option]Gaëtan Gilbert
2020-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ...coqbot-app[bot]
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-10-02Merge PR #13106: Remove the forward class hint feature.coqbot-app[bot]
2020-10-01Merge PR #13108: Getting rid of temerarious EConstr.to_constr in Himsgcoqbot-app[bot]
2020-10-01Merge PR #13114: Reimplement Admit Obligations using standard Admitted codecoqbot-app[bot]
2020-10-01Merge PR #13116: interp_context_evars: removed unused [shift] argumentcoqbot-app[bot]
2020-10-01Merge PR #13123: Fix combining uniform parameters and mutual inductives.coqbot-app[bot]
2020-09-30Fix combining uniform parameters and mutual inductives.Jasper Hugunin
2020-09-30Further simplification of the typeclass registration API.Pierre-Marie Pédrot
2020-09-30Remove the forward class hint feature.Pierre-Marie Pédrot
2020-09-30interp_context_evars: removed unused [shift] argumentGaëtan Gilbert
2020-09-30Reimplement Admit Obligations using standard Admitted codeGaëtan Gilbert
2020-09-28Getting rid of temerarious EConstr.to_constr in Himsg.Hugo Herbelin
2020-09-28More precise information when unification fails because of incompatible candi...Hugo Herbelin
2020-09-23Merge PR #12977: Statically ensure that only polymophic hint terms come with ...coqbot-app[bot]
2020-09-23Merge 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 / checkEmilio Jesus Gallego Arias
2020-09-15A temporary fix of #13018 and #12775 for branch 8.2.Hugo Herbelin
2020-09-13Statically ensure that only polymophic hint terms come with a context.Pierre-Marie Pédrot
2020-09-10When a notation is only parsing, do not attach to it a specific format.Hugo Herbelin
2020-09-09Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable fro...Pierre-Marie Pédrot
2020-09-08Merge PR #12931: Proof using cleanup, small doc addition and fix using Type i...coqbot-app[bot]
2020-09-07Circumvent revealed bug of evar resolution for fixpointMaxime Dénès
2020-09-03Fix incorrect debruijn handling when Record calls maybe_unify_params_inGaëtan Gilbert
2020-09-01Unify the shelvesMaxime Dénès
2020-09-01Merge PR #12892: Update update_global_env usagePierre-Marie Pédrot
2020-08-31[declare] Return both declared constants in Derive path.Emilio Jesus Gallego Arias
2020-08-31Update update_global_env usageGaëtan Gilbert
2020-08-28About: Add a mention that arguments have been renamed, if ever it is the case.Hugo Herbelin
2020-08-28Where there are several lists of implicit arguments, don't pretend names matter.Hugo Herbelin
2020-08-28Do not write "rename" for arguments in About, since these arguments are valid...Hugo Herbelin
2020-08-28When printing the type in About, use the renamed arguments.Hugo Herbelin
2020-08-28When reporting an implicit argument error on a rename argument, use the renam...Hugo Herbelin
2020-08-28In "About", print all arguments, even if it is trailing list of _.Hugo Herbelin
2020-08-28Proof using cleanup, small doc addition and fix using Type in collectionsGaëtan Gilbert
2020-08-27[state] A few nits after consolidation of state.Emilio Jesus Gallego Arias
2020-08-27Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfooPierre-Marie Pédrot
2020-08-26Wrap future goals into a moduleMaxime Dénès
2020-08-26Make future_goals stack explicit in the evarmapMaxime Dénès
2020-08-26Move given_up goals to evar_mapMaxime Dénès
2020-08-25Moving production_level_eq to extend.ml for separation of concerns.Hugo Herbelin
2020-08-25A fix and two enhancements of trailing pattern factorization in rec. notations.Hugo Herbelin
2020-08-25Fix slow Print Universes Subgraph when many ambient universes.Gaëtan Gilbert
2020-08-24Update sigma instead of erasing it in `update_global_env`Maxime Dénès
2020-08-22Merge PR #12866: Less fragile scheme equalityHugo Herbelin
2020-08-21Merge PR #12759: [vernac] refine check for unresolved evarscoqbot
2020-08-20Use properly fresh names for Scheme EqualityJasper Hugunin
2020-08-20Merge PR #12756: Do not refresh the names of implicit arguments.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 11:13:40 +0000