aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2020-11-04Encapsulate the last use of IsConstr in the Hints API.Pierre-Marie Pédrot
2020-11-03Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding not...coqbot-app[bot]
2020-11-02[doc] attribute #[using]Enrico Tassi
2020-11-02[stm] support #[using] attributeEnrico Tassi
2020-11-02document Proof.compactEnrico Tassi
2020-11-02attribute #[using] for Definition and FixpointEnrico Tassi
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-27Merge PR #13075: Introducing the foundations for a name-alias-agnostic APIcoqbot-app[bot]
2020-10-26Improve tactic interpreter registration API a bitGaëtan Gilbert
2020-10-23[declare] Remove recursive declaration from non-recursive functionsEmilio Jesus Gallego Arias
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
2020-10-21Deprecate the non-qualified equality functions on kerpairs.Pierre-Marie Pédrot
2020-10-21Merge PR #13118: [type classes] Simplify cl_contextPierre-Marie Pédrot
2020-10-19Addressing parsing part #13078.Hugo Herbelin
2020-10-19Fixing printing part of #13078 (anomaly with binding notations in patterns).Hugo Herbelin
2020-10-16Fixes/enhancements with local definitions in records.Hugo Herbelin
2020-10-16Generalizing and exporting interp_assumption/interp_definition.Hugo Herbelin
2020-10-15Merge PR #12925: [declare] Fix types of mutual lemmas when using Admitted.coqbot-app[bot]
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-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]
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 07:13:09 +0000