aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacentries.ml
AgeCommit message (Expand)Author
2021-04-14Put async worker id in universe namesGaëtan Gilbert
2021-04-06One catch-all's missing a noncritical; another is now useless (see 7efaf86).Hugo Herbelin
2021-03-04[notation] option to fine tune printing of literalsEnrico Tassi
2021-02-25[proof using] Remove duplicate code, refactor.Emilio Jesus Gallego Arias
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-17Merge PR #13734: Fix #13732: Implicit Type vs universesPierre-Marie Pédrot
2021-02-11[vernac] pass the loc of the whole command to the interp functionEnrico Tassi
2021-01-26[vernac] Check that no proofs do remain open at section/module closing timeEmilio Jesus Gallego Arias
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
2021-01-11Fix #13732: Implicit Type vs universesGaëtan Gilbert
2021-01-06Further pushing up the printing and sorting of universes.Pierre-Marie Pédrot
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:07:29 +0000