aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacentries.ml
AgeCommit message (Expand)Author
2020-11-26[environ] [typing_flags] Introduce helper function to remove duplicate codeEmilio Jesus Gallego Arias
2020-11-26[vernac] Allow to control typing flags with attributes.Emilio Jesus Gallego Arias
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-11-18[attributes] Update error message referring to deprecated syntax.Emilio Jesus Gallego Arias
2020-11-18[attributes] Allow boolean, single-value attributes.Emilio Jesus Gallego Arias
2020-11-16Warning on hint commands that have no explicit locality.Pierre-Marie Pédrot
2020-11-16Merge PR #13388: Export locality for all hint commandscoqbot-app[bot]
2020-11-15Implement export locality for the remaining Hint commands.Pierre-Marie Pédrot
2020-11-13[record] Cleanup of data structure and functions [1/2]Emilio Jesus Gallego Arias
2020-11-12Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ...Pierre-Marie Pédrot
2020-11-05Merge PR #13191: Fix anomaly when importing a functorPierre-Marie Pédrot
2020-11-04Moving interpretation of user-level universes in constrintern.ml.Hugo Herbelin
2020-11-02[doc] attribute #[using]Enrico Tassi
2020-11-02attribute #[using] for Definition and FixpointEnrico Tassi
2020-10-16Fixes/enhancements with local definitions in records.Hugo Herbelin
2020-10-14Fix anomaly when importing a functorGaëtan Gilbert
2020-10-10Print Scope & cie: Add parentheses around notation interpretation.Hugo Herbelin
2020-10-06Define a new type instance_flag instead of using [unit option]Gaëtan Gilbert
2020-09-30Remove the forward class hint feature.Pierre-Marie Pédrot
2020-09-15[vernac] Don't allow attributes on print / checkEmilio Jesus Gallego Arias
2020-09-01Unify the shelvesMaxime Dénès
2020-08-27Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfooPierre-Marie Pédrot
2020-08-26Move given_up goals to evar_mapMaxime Dénès
2020-08-25Fix slow Print Universes Subgraph when many ambient universes.Gaëtan Gilbert
2020-08-18Rename VM-related kernel/cfoo files to kernel/vmfooGaëtan Gilbert
2020-07-08[obligations] Functionalize Program stateEmilio Jesus Gallego Arias
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
2020-07-01[state] Consolidate state handling in VernacstateEmilio Jesus Gallego Arias
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-30[declaremods] Remove abstraction of imperative module operationsEmilio Jesus Gallego Arias
2020-06-26[recLemmas] Nit on naming consistency.Emilio Jesus Gallego Arias
2020-06-26[declare] Return list of declared global in Proof.saveEmilio Jesus Gallego Arias
2020-06-26[declare] Merge remaining obligations bits into DeclareEmilio Jesus Gallego Arias
2020-06-26[declare] Improve organization of proof/constant information.Emilio Jesus Gallego Arias
2020-06-26[vernac] Nit refatoring on lemma command interpretationEmilio Jesus Gallego Arias
2020-06-26[declare] Use Recthm.t in mutual analysis functionsEmilio Jesus Gallego Arias
2020-06-26[declare] Refactor analysis and construction of mutual lemmasEmilio Jesus Gallego Arias
2020-06-26[declare] Reify Proof.t API into the Proof module.Emilio Jesus Gallego Arias
2020-06-26[declare] [api] Removal of duplicated type aliases.Emilio Jesus Gallego Arias
2020-06-26[declare] Refactor constant information into a record.Emilio Jesus Gallego Arias
2020-06-26[declare] Remove mutual internals from Info.t structure.Emilio Jesus Gallego Arias
2020-06-26[declare] Move proof information to declare.Emilio Jesus Gallego Arias
2020-05-29Require in Section: warning is now about fragility not deprecation.Gaëtan Gilbert
2020-05-18[declare] Merge `DeclareObl` into `Declare`Emilio Jesus Gallego Arias
2020-05-18[obligations] Pre-functionalize Program stateEmilio Jesus Gallego Arias
2020-05-15Moving interpretation of Search commands to their own file: comSearch.ml.Hugo Herbelin
2020-05-15Cleaning the use of pstate and evar_map in Search.Hugo Herbelin
2020-05-15Search: Displaying the "use About" notice only when really needed.Hugo Herbelin
2020-05-15Addressing a suggestion from Théo Zimmermann.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:41:52 +0000