aboutsummaryrefslogtreecommitdiff
path: root/vernac/class.ml
AgeCommit message (Expand)Author
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-01[declare] Separate kinds from entries in constant declarationEmilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-06-26[declare] Fine tuning of Hook type.Emilio Jesus Gallego Arias
2019-06-24[api] Remove `polymorphic` type alias, use labels instead.Emilio Jesus Gallego Arias
2019-06-24[api] Move `locality` from `library` to `vernac`.Emilio Jesus Gallego Arias
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-06-20Merge PR #9645: [proof] Remove terminator type, unifying regular and obligati...Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17[proof] Move declaration hooks to DeclareDef.Emilio Jesus Gallego Arias
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-04-10Functionalize env in type classesMaxime Dénès
2019-04-10Move vernac-related part of coercions to vernacMaxime Dénès
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-23[vernac] Unify declaration hooks.Emilio Jesus Gallego Arias
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-10-26Merge PR #8687: Mini reorganization type of global constr of globalPierre-Marie Pédrot
2018-10-19Deprecating Global.type_of_global_in_context.Hugo Herbelin
2018-10-18[api] Qualify access to `Nametab`Emilio Jesus Gallego Arias
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-03Allow “Let”-defined coercionsVincent Laporte
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-03-09allow Prop as source for coercionscharguer
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-24Use Entries.constant_universes_entry more.Gaëtan Gilbert
2017-11-24Stop exposing UState.universe_context and its Evd wrapper.Gaëtan Gilbert
2017-11-24Separate checking univ_decls and obtaining universe binder names.Gaëtan Gilbert
2017-11-14Fixes #6129 (declaration of coercions made compatible with local definitions).Hugo Herbelin
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-09-19Don't lose names in UState.universe_context.Gaëtan Gilbert
2017-07-13Remove the function Global.type_of_global_unsafe.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-27Fix omitted labels in function callsGaetan Gilbert
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:03:22 +0000