aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2020-10-15Merge PR #13181: Guard unify_leq_delay calls in TypingPierre-Marie Pédrot
2020-10-15Merge PR #13144: Closes #13142: more standardized pretty-printing of Coq recordscoqbot-app[bot]
2020-10-15[declare] Fix types of mutual lemmas when using Admitted.Emilio Jesus Gallego Arias
2020-10-14Fix anomaly when importing a functorGaëtan Gilbert
2020-10-12Catch more errors in Unification.abstract_list_allGaëtan Gilbert
2020-10-10Adding a warning in case a notation is used neither for parsing nor printing.Hugo Herbelin
2020-10-10Notations: reworking the treatment of only-parsing and only-printing notations.Hugo Herbelin
2020-10-10Print Scope & cie: Add parentheses around notation interpretation.Hugo Herbelin
2020-10-10Closes #13142 (more standardized pretty-printing of records).Hugo Herbelin
2020-10-09Merge PR #13088: [stm] move par: to comTacticcoqbot-app[bot]
2020-10-09[stm] move par: implementation to vernac/comTactic and stm/partacEnrico Tassi
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
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-06Remove unused is_class info from cl_contextGaëtan Gilbert
2020-10-06First list in cl_context is just booleansGaë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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:03:01 +0000